Finite filtrations and reflection of linear isomorphisms

A linear map which is bijective on a filtration term and on the next successive quotient is bijective on the next term. Iterating this elementary fact is the linear-algebra endpoint of the finite elementary-interval filtration used by string detectors.

def MagnitudeConjecture.LinearAlgebra.FiniteFiltration.restrictionMap {k V W : Type u} [Field k] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] (f : V →ₗ[k] W) (U : Submodule k V) (U' : Submodule k W) (h : Submodule.map f U ≤ U') : ↥U →ₗ[k] ↥U'

Restrict a linear map to specified source and target subspaces.

@[simp]

theorem MagnitudeConjecture.LinearAlgebra.FiniteFiltration.restrictionMap_coe {k V W : Type u} [Field k] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] (f : V →ₗ[k] W) (U : Submodule k V) (U' : Submodule k W) (h : Submodule.map f U ≤ U') (x : ↥U) : ↑((restrictionMap f U U' h) x) = f ↑x

def MagnitudeConjecture.LinearAlgebra.FiniteFiltration.layerMap {k V W : Type u} [Field k] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] (f : V →ₗ[k] W) (U X : Submodule k V) (U' X' : Submodule k W) (_hUX : U ≤ X) (_hU'X' : U' ≤ X') (hX : Submodule.map f X ≤ X') (hU : Submodule.map f U ≤ U') : ↥X ⧸ Submodule.comap X.subtype U →ₗ[k] ↥X' ⧸ Submodule.comap X'.subtype U'

The map induced on one successive quotient of two compatible filtered spaces.

@[simp]

theorem MagnitudeConjecture.LinearAlgebra.FiniteFiltration.layerMap_mk {k V W : Type u} [Field k] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] (f : V →ₗ[k] W) (U X : Submodule k V) (U' X' : Submodule k W) (hUX : U ≤ X) (hU'X' : U' ≤ X') (hX : Submodule.map f X ≤ X') (hU : Submodule.map f U ≤ U') (x : ↥X) : (layerMap f U X U' X' hUX hU'X' hX hU) (Submodule.Quotient.mk x) = Submodule.Quotient.mk ((restrictionMap f X X' hX) x)

theorem MagnitudeConjecture.LinearAlgebra.FiniteFiltration.restrictionMap_bijective_of_layerMap_bijective {k V W : Type u} [Field k] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] (f : V →ₗ[k] W) (U X : Submodule k V) (U' X' : Submodule k W) (hUX : U ≤ X) (hU'X' : U' ≤ X') (hX : Submodule.map f X ≤ X') (hU : Submodule.map f U ≤ U') (hbase : Function.Bijective ⇑(restrictionMap f U U' hU)) (hlayer : Function.Bijective ⇑(layerMap f U X U' X' hUX hU'X' hX hU)) : Function.Bijective ⇑(restrictionMap f X X' hX)

Bijectivity on one filtration term and the following quotient implies bijectivity on the following term.

structure MagnitudeConjecture.LinearAlgebra.FiniteFiltration.Filtration (k V : Type u) [Field k] [AddCommGroup V] [Module k V] (n : ℕ) : Type u

A finite increasing filtration from zero to the whole vector space. The natural number n is the number of successive layers.

• subspace : Fin (n + 1) → Submodule k V
• monotone_subspace : Monotone self.subspace
• subspace_zero : self.subspace 0 = ⊥
• subspace_last : self.subspace (Fin.last n) = ⊤

def MagnitudeConjecture.LinearAlgebra.FiniteFiltration.Filtration.Compatible {k V W : Type u} [Field k] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] {n : ℕ} (f : V →ₗ[k] W) (F : Filtration k V n) (G : Filtration k W n) : Prop

A linear map preserves two filtrations with the same finite index.

def MagnitudeConjecture.LinearAlgebra.FiniteFiltration.Filtration.gradedMap {k V W : Type u} [Field k] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] {n : ℕ} (f : V →ₗ[k] W) (F : Filtration k V n) (G : Filtration k W n) (h : Compatible f F G) (i : Fin n) : ↥(F.subspace i.succ) ⧸ Submodule.comap (F.subspace i.succ).subtype (F.subspace i.castSucc) →ₗ[k] ↥(G.subspace i.succ) ⧸ Submodule.comap (G.subspace i.succ).subtype (G.subspace i.castSucc)

The map induced on the ith successive filtration quotient.

theorem MagnitudeConjecture.LinearAlgebra.FiniteFiltration.Filtration.map_bijective_of_gradedMap_bijective {k V W : Type u} [Field k] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] {n : ℕ} (f : V →ₗ[k] W) (F : Filtration k V n) (G : Filtration k W n) (h : Compatible f F G) (hgraded : ∀ (i : Fin n), Function.Bijective ⇑(gradedMap f F G h i)) : Function.Bijective ⇑f

Bijectivity on every successive quotient of two compatible finite filtrations implies bijectivity of the original linear map.