Commit 2023-12-18 16:03 a3e8d01e

View on Github →

feat: injective bilinear pairing V→W* with V f.d. induces surjective W→V* (#8820) From the Hairer challenge

add flip_in/sur/bijective_iff₁₂: if either of the spaces V and W is finite-dimensional, a linear map V → W* is injective/surjective/bijective iff the flipped map W → V* is surjective/injective/bijective.
also add consequence for SeparatingDual from the projective space thread (cc @smorel394)
remove the FiniteDimensional condition from dual_finrank_eq, finrank_range_dualMap_eq_finrank_range, and dualMap_injective/bijective_iff, completing two TODO items by @kmill
add two lemmas toDual_injective and finite_dual_iff
golf several proofs in LinearAlgebra/Dual

Estimated changes

Modified Mathlib/Analysis/NormedSpace/HahnBanach/SeparatingDual.lean

added theorem SeparatingDual.dualMap_surjective_iff

added theorem separatingDual_iff_injective

Modified Mathlib/LinearAlgebra/Dimension.lean

added theorem LinearIndependent.finite_of_le_span_finite

modified def Submodule.inductionOnRank

deleted def linearIndependentFintypeOfLeSpanFintype

Modified Mathlib/LinearAlgebra/Dual.lean

modified theorem Basis.toDual_inj

added theorem Basis.toDual_injective

modified def LinearEquiv.dualMap

added theorem LinearMap.flip_bijective_iff₁

added theorem LinearMap.flip_bijective_iff₂

added theorem LinearMap.flip_injective_iff₁

added theorem LinearMap.flip_injective_iff₂

added theorem LinearMap.flip_surjective_iff₁

added theorem LinearMap.flip_surjective_iff₂

modified theorem Module.apply_evalEquiv_symm_apply

modified theorem Module.bijective_dual_eval

added theorem Module.finite_dual_iff

modified theorem Subspace.dualLift_of_subtype