Moving a two-filtration subquotient across a linear map #

For nested subspaces A⁻ ≤ A⁺ in the source and B⁻ ≤ B⁺ in the target, a linear map identifies the two naturally corresponding subquotients built from image and preimage. This is the linear-algebra step in Ringel's proof that a string detector does not depend on the chosen split position.

source

def MagnitudeConjecture.LinearAlgebra.PairSubquotient.quotientEquivOfEq {k V : Type u} [Field k] [AddCommGroup V] [Module k V] (U U' D D' : Submodule k V) (hU : U = U') (hD : D = D') :

(↥U ⧸ Submodule.comap U.subtype D) ≃ₗ[k] ↥U' ⧸ Submodule.comap U'.subtype D'

Transport a subquotient across equal numerator and denominator submodules.

Instances For

source

@[simp]

theorem MagnitudeConjecture.LinearAlgebra.PairSubquotient.quotientEquivOfEq_apply_mk {k V : Type u} [Field k] [AddCommGroup V] [Module k V] (U U' D D' : Submodule k V) (hU : U = U') (hD : D = D') (x : ↥U) :

(quotientEquivOfEq U U' D D' hU hD) (Submodule.Quotient.mk x) = Submodule.Quotient.mk ⟨↑x, ⋯⟩

source

def MagnitudeConjecture.LinearAlgebra.PairSubquotient.sourceNumerator {k V W : Type u} [Field k] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] (f : V →ₗ[k] W) (Aplus : Submodule k V) (Bplus : Submodule k W) :

Submodule k V

Numerator before moving across f.

Instances For

source

def MagnitudeConjecture.LinearAlgebra.PairSubquotient.sourceDenominator {k V W : Type u} [Field k] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] (f : V →ₗ[k] W) (Aminus Aplus : Submodule k V) (Bminus Bplus : Submodule k W) :

Submodule k V

Denominator before moving across f.

Instances For

source

def MagnitudeConjecture.LinearAlgebra.PairSubquotient.targetNumerator {k V W : Type u} [Field k] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] (f : V →ₗ[k] W) (Aplus : Submodule k V) (Bplus : Submodule k W) :

Submodule k W

Numerator after moving across f.

Instances For

source

def MagnitudeConjecture.LinearAlgebra.PairSubquotient.targetDenominator {k V W : Type u} [Field k] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] (f : V →ₗ[k] W) (Aminus Aplus : Submodule k V) (Bminus Bplus : Submodule k W) :

Submodule k W

Denominator after moving across f.

Instances For

source

theorem MagnitudeConjecture.LinearAlgebra.PairSubquotient.sourceDenominator_le_sourceNumerator {k V W : Type u} [Field k] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] (f : V →ₗ[k] W) (Aminus Aplus : Submodule k V) (Bminus Bplus : Submodule k W) (hA : Aminus ≤ Aplus) (hB : Bminus ≤ Bplus) :

sourceDenominator f Aminus Aplus Bminus Bplus ≤ sourceNumerator f Aplus Bplus

source

theorem MagnitudeConjecture.LinearAlgebra.PairSubquotient.targetDenominator_le_targetNumerator {k V W : Type u} [Field k] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] (f : V →ₗ[k] W) (Aminus Aplus : Submodule k V) (Bminus Bplus : Submodule k W) (hA : Aminus ≤ Aplus) (hB : Bminus ≤ Bplus) :

targetDenominator f Aminus Aplus Bminus Bplus ≤ targetNumerator f Aplus Bplus

source

def MagnitudeConjecture.LinearAlgebra.PairSubquotient.sourceDenominatorInNumerator {k V W : Type u} [Field k] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] (f : V →ₗ[k] W) (Aminus Aplus : Submodule k V) (Bminus Bplus : Submodule k W) :

Submodule k ↥(sourceNumerator f Aplus Bplus)

The source denominator inside its numerator.

Instances For

source

def MagnitudeConjecture.LinearAlgebra.PairSubquotient.targetDenominatorInNumerator {k V W : Type u} [Field k] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] (f : V →ₗ[k] W) (Aminus Aplus : Submodule k V) (Bminus Bplus : Submodule k W) :

Submodule k ↥(targetNumerator f Aplus Bplus)

The target denominator inside its numerator.

Instances For

source

def MagnitudeConjecture.LinearAlgebra.PairSubquotient.numeratorMap {k V W : Type u} [Field k] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] (f : V →ₗ[k] W) (Aplus : Submodule k V) (Bplus : Submodule k W) :

↥(sourceNumerator f Aplus Bplus) →ₗ[k] ↥(targetNumerator f Aplus Bplus)

Restriction of f to the two numerators.

Instances For

source

@[simp]

theorem MagnitudeConjecture.LinearAlgebra.PairSubquotient.numeratorMap_coe {k V W : Type u} [Field k] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] (f : V →ₗ[k] W) (Aplus : Submodule k V) (Bplus : Submodule k W) (x : ↥(sourceNumerator f Aplus Bplus)) :

↑((numeratorMap f Aplus Bplus) x) = f ↑x

source

theorem MagnitudeConjecture.LinearAlgebra.PairSubquotient.denominator_map_le {k V W : Type u} [Field k] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] (f : V →ₗ[k] W) (Aminus Aplus : Submodule k V) (Bminus Bplus : Submodule k W) (_hA : Aminus ≤ Aplus) (_hB : Bminus ≤ Bplus) :

Submodule.map (numeratorMap f Aplus Bplus) (sourceDenominatorInNumerator f Aminus Aplus Bminus Bplus) ≤ targetDenominatorInNumerator f Aminus Aplus Bminus Bplus

source

def MagnitudeConjecture.LinearAlgebra.PairSubquotient.quotientMap {k V W : Type u} [Field k] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] (f : V →ₗ[k] W) (Aminus Aplus : Submodule k V) (Bminus Bplus : Submodule k W) (hA : Aminus ≤ Aplus) (hB : Bminus ≤ Bplus) :

↥(sourceNumerator f Aplus Bplus) ⧸ sourceDenominatorInNumerator f Aminus Aplus Bminus Bplus →ₗ[k] ↥(targetNumerator f Aplus Bplus) ⧸ targetDenominatorInNumerator f Aminus Aplus Bminus Bplus

The linear map between the two subquotients.

Instances For

source

@[simp]

theorem MagnitudeConjecture.LinearAlgebra.PairSubquotient.quotientMap_mk {k V W : Type u} [Field k] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] (f : V →ₗ[k] W) (Aminus Aplus : Submodule k V) (Bminus Bplus : Submodule k W) (hA : Aminus ≤ Aplus) (hB : Bminus ≤ Bplus) (x : ↥(sourceNumerator f Aplus Bplus)) :

(quotientMap f Aminus Aplus Bminus Bplus hA hB) (Submodule.Quotient.mk x) = Submodule.Quotient.mk ((numeratorMap f Aplus Bplus) x)

source

theorem MagnitudeConjecture.LinearAlgebra.PairSubquotient.quotientMap_surjective {k V W : Type u} [Field k] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] (f : V →ₗ[k] W) (Aminus Aplus : Submodule k V) (Bminus Bplus : Submodule k W) (hA : Aminus ≤ Aplus) (hB : Bminus ≤ Bplus) :

Function.Surjective ⇑(quotientMap f Aminus Aplus Bminus Bplus hA hB)

source

theorem MagnitudeConjecture.LinearAlgebra.PairSubquotient.quotientMap_injective {k V W : Type u} [Field k] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] (f : V →ₗ[k] W) (Aminus Aplus : Submodule k V) (Bminus Bplus : Submodule k W) (hA : Aminus ≤ Aplus) (hB : Bminus ≤ Bplus) :

Function.Injective ⇑(quotientMap f Aminus Aplus Bminus Bplus hA hB)

source

noncomputable def MagnitudeConjecture.LinearAlgebra.PairSubquotient.quotientEquiv {k V W : Type u} [Field k] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] (f : V →ₗ[k] W) (Aminus Aplus : Submodule k V) (Bminus Bplus : Submodule k W) (hA : Aminus ≤ Aplus) (hB : Bminus ≤ Bplus) :

(↥(sourceNumerator f Aplus Bplus) ⧸ sourceDenominatorInNumerator f Aminus Aplus Bminus Bplus) ≃ₗ[k] ↥(targetNumerator f Aplus Bplus) ⧸ targetDenominatorInNumerator f Aminus Aplus Bminus Bplus

Moving the split across one linear map gives a linear equivalence of the two pair subquotients.

Instances For

source

def MagnitudeConjecture.LinearAlgebra.PairSubquotient.swappedSourceNumerator {k V W : Type u} [Field k] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] (f : V →ₗ[k] W) (Aplus : Submodule k V) (Bplus : Submodule k W) :

Submodule k V

Source numerator with the two filtrations written in the opposite order.

Instances For

source

def MagnitudeConjecture.LinearAlgebra.PairSubquotient.swappedSourceDenominator {k V W : Type u} [Field k] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] (f : V →ₗ[k] W) (Aminus Aplus : Submodule k V) (Bminus Bplus : Submodule k W) :

Submodule k V

Source denominator with the two filtrations written in the opposite order.

Instances For

source

def MagnitudeConjecture.LinearAlgebra.PairSubquotient.swappedTargetNumerator {k V W : Type u} [Field k] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] (f : V →ₗ[k] W) (Aplus : Submodule k V) (Bplus : Submodule k W) :

Submodule k W

Target numerator with the two filtrations written in the opposite order.

Instances For

source

def MagnitudeConjecture.LinearAlgebra.PairSubquotient.swappedTargetDenominator {k V W : Type u} [Field k] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] (f : V →ₗ[k] W) (Aminus Aplus : Submodule k V) (Bminus Bplus : Submodule k W) :

Submodule k W

Target denominator with the two filtrations written in the opposite order.

Instances For

source

def MagnitudeConjecture.LinearAlgebra.PairSubquotient.swappedNumeratorMap {k V W : Type u} [Field k] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] (f : V →ₗ[k] W) (Aplus : Submodule k V) (Bplus : Submodule k W) :

↥(swappedSourceNumerator f Aplus Bplus) →ₗ[k] ↥(swappedTargetNumerator f Aplus Bplus)

Restriction of f between the swapped numerators.

Instances For

source

@[simp]

theorem MagnitudeConjecture.LinearAlgebra.PairSubquotient.swappedNumeratorMap_coe {k V W : Type u} [Field k] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] (f : V →ₗ[k] W) (Aplus : Submodule k V) (Bplus : Submodule k W) (x : ↥(swappedSourceNumerator f Aplus Bplus)) :

↑((swappedNumeratorMap f Aplus Bplus) x) = f ↑x

source

def MagnitudeConjecture.LinearAlgebra.PairSubquotient.swappedSourceDenominatorInNumerator {k V W : Type u} [Field k] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] (f : V →ₗ[k] W) (Aminus Aplus : Submodule k V) (Bminus Bplus : Submodule k W) :

Submodule k ↥(swappedSourceNumerator f Aplus Bplus)

Swapped source denominator inside its numerator.

Instances For

source

def MagnitudeConjecture.LinearAlgebra.PairSubquotient.swappedTargetDenominatorInNumerator {k V W : Type u} [Field k] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] (f : V →ₗ[k] W) (Aminus Aplus : Submodule k V) (Bminus Bplus : Submodule k W) :

Submodule k ↥(swappedTargetNumerator f Aplus Bplus)

Swapped target denominator inside its numerator.

Instances For

source

theorem MagnitudeConjecture.LinearAlgebra.PairSubquotient.swappedDenominator_map_le {k V W : Type u} [Field k] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] (f : V →ₗ[k] W) (Aminus Aplus : Submodule k V) (Bminus Bplus : Submodule k W) :

Submodule.map (swappedNumeratorMap f Aplus Bplus) (swappedSourceDenominatorInNumerator f Aminus Aplus Bminus Bplus) ≤ swappedTargetDenominatorInNumerator f Aminus Aplus Bminus Bplus

source

def MagnitudeConjecture.LinearAlgebra.PairSubquotient.swappedQuotientMap {k V W : Type u} [Field k] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] (f : V →ₗ[k] W) (Aminus Aplus : Submodule k V) (Bminus Bplus : Submodule k W) :

↥(swappedSourceNumerator f Aplus Bplus) ⧸ swappedSourceDenominatorInNumerator f Aminus Aplus Bminus Bplus →ₗ[k] ↥(swappedTargetNumerator f Aplus Bplus) ⧸ swappedTargetDenominatorInNumerator f Aminus Aplus Bminus Bplus

Explicit quotient map between the swapped pair subquotients.

Instances For

source

@[simp]

theorem MagnitudeConjecture.LinearAlgebra.PairSubquotient.swappedQuotientMap_mk {k V W : Type u} [Field k] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] (f : V →ₗ[k] W) (Aminus Aplus : Submodule k V) (Bminus Bplus : Submodule k W) (x : ↥(swappedSourceNumerator f Aplus Bplus)) :

(swappedQuotientMap f Aminus Aplus Bminus Bplus) (Submodule.Quotient.mk x) = Submodule.Quotient.mk ((swappedNumeratorMap f Aplus Bplus) x)

source

theorem MagnitudeConjecture.LinearAlgebra.PairSubquotient.swappedQuotientMap_surjective {k V W : Type u} [Field k] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] (f : V →ₗ[k] W) (Aminus Aplus : Submodule k V) (Bminus Bplus : Submodule k W) :

Function.Surjective ⇑(swappedQuotientMap f Aminus Aplus Bminus Bplus)

source

theorem MagnitudeConjecture.LinearAlgebra.PairSubquotient.swappedQuotientMap_injective {k V W : Type u} [Field k] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] (f : V →ₗ[k] W) (Aminus Aplus : Submodule k V) (Bminus Bplus : Submodule k W) (hA : Aminus ≤ Aplus) :

Function.Injective ⇑(swappedQuotientMap f Aminus Aplus Bminus Bplus)

source

noncomputable def MagnitudeConjecture.LinearAlgebra.PairSubquotient.quotientEquivSwapped {k V W : Type u} [Field k] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] (f : V →ₗ[k] W) (Aminus Aplus : Submodule k V) (Bminus Bplus : Submodule k W) (hA : Aminus ≤ Aplus) (_hB : Bminus ≤ Bplus) :

(↥(swappedSourceNumerator f Aplus Bplus) ⧸ Submodule.comap (swappedSourceNumerator f Aplus Bplus).subtype (swappedSourceDenominator f Aminus Aplus Bminus Bplus)) ≃ₗ[k] ↥(swappedTargetNumerator f Aplus Bplus) ⧸ Submodule.comap (swappedTargetNumerator f Aplus Bplus).subtype (swappedTargetDenominator f Aminus Aplus Bminus Bplus)

The same image/preimage equivalence when both pair filtrations are written in the opposite order.

Instances For

source

@[simp]

theorem MagnitudeConjecture.LinearAlgebra.PairSubquotient.quotientEquiv_apply_mk {k V W : Type u} [Field k] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] (f : V →ₗ[k] W) (Aminus Aplus : Submodule k V) (Bminus Bplus : Submodule k W) (hA : Aminus ≤ Aplus) (hB : Bminus ≤ Bplus) (x : ↥(sourceNumerator f Aplus Bplus)) :

(quotientEquiv f Aminus Aplus Bminus Bplus hA hB) (Submodule.Quotient.mk x) = Submodule.Quotient.mk ((numeratorMap f Aplus Bplus) x)

source

@[simp]

theorem MagnitudeConjecture.LinearAlgebra.PairSubquotient.quotientEquivSwapped_apply_mk {k V W : Type u} [Field k] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] (f : V →ₗ[k] W) (Aminus Aplus : Submodule k V) (Bminus Bplus : Submodule k W) (hA : Aminus ≤ Aplus) (hB : Bminus ≤ Bplus) (x : ↥(swappedSourceNumerator f Aplus Bplus)) :

(quotientEquivSwapped f Aminus Aplus Bminus Bplus hA hB) (Submodule.Quotient.mk x) = Submodule.Quotient.mk ((swappedNumeratorMap f Aplus Bplus) x)

source

noncomputable def MagnitudeConjecture.LinearAlgebra.PairSubquotient.quotientEquivIdentified {k V W : Type u} [Field k] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] (f : V →ₗ[k] W) (Aminus Aplus : Submodule k V) (Bminus Bplus : Submodule k W) (U D : Submodule k V) (U' D' : Submodule k W) (hSourceNum : U = sourceNumerator f Aplus Bplus) (hSourceDen : D = sourceDenominator f Aminus Aplus Bminus Bplus) (hTargetNum : targetNumerator f Aplus Bplus = U') (hTargetDen : targetDenominator f Aminus Aplus Bminus Bplus = D') (hA : Aminus ≤ Aplus) (hB : Bminus ≤ Bplus) :

(↥U ⧸ Submodule.comap U.subtype D) ≃ₗ[k] ↥U' ⧸ Submodule.comap U'.subtype D'

Move a pair subquotient across f after identifying the displayed source and target numerators and denominators with the generic image/preimage pair.

Instances For

source

@[simp]

theorem MagnitudeConjecture.LinearAlgebra.PairSubquotient.quotientEquivIdentified_apply_mk {k V W : Type u} [Field k] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] (f : V →ₗ[k] W) (Aminus Aplus : Submodule k V) (Bminus Bplus : Submodule k W) (U D : Submodule k V) (U' D' : Submodule k W) (hSourceNum : U = sourceNumerator f Aplus Bplus) (hSourceDen : D = sourceDenominator f Aminus Aplus Bminus Bplus) (hTargetNum : targetNumerator f Aplus Bplus = U') (hTargetDen : targetDenominator f Aminus Aplus Bminus Bplus = D') (hA : Aminus ≤ Aplus) (hB : Bminus ≤ Bplus) (x : ↥U) :

(quotientEquivIdentified f Aminus Aplus Bminus Bplus U D U' D' hSourceNum hSourceDen hTargetNum hTargetDen hA hB) (Submodule.Quotient.mk x) = Submodule.Quotient.mk ⟨f ↑x, ⋯⟩

source

noncomputable def MagnitudeConjecture.LinearAlgebra.PairSubquotient.quotientEquivSwappedIdentified {k V W : Type u} [Field k] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] (f : V →ₗ[k] W) (Aminus Aplus : Submodule k V) (Bminus Bplus : Submodule k W) (U D : Submodule k V) (U' D' : Submodule k W) (hSourceNum : U = swappedSourceNumerator f Aplus Bplus) (hSourceDen : D = swappedSourceDenominator f Aminus Aplus Bminus Bplus) (hTargetNum : swappedTargetNumerator f Aplus Bplus = U') (hTargetDen : swappedTargetDenominator f Aminus Aplus Bminus Bplus = D') (hA : Aminus ≤ Aplus) (hB : Bminus ≤ Bplus) :

(↥U ⧸ Submodule.comap U.subtype D) ≃ₗ[k] ↥U' ⧸ Submodule.comap U'.subtype D'

The identified form of quotientEquivSwapped.

Instances For

source

@[simp]

theorem MagnitudeConjecture.LinearAlgebra.PairSubquotient.quotientEquivSwappedIdentified_apply_mk {k V W : Type u} [Field k] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] (f : V →ₗ[k] W) (Aminus Aplus : Submodule k V) (Bminus Bplus : Submodule k W) (U D : Submodule k V) (U' D' : Submodule k W) (hSourceNum : U = swappedSourceNumerator f Aplus Bplus) (hSourceDen : D = swappedSourceDenominator f Aminus Aplus Bminus Bplus) (hTargetNum : swappedTargetNumerator f Aplus Bplus = U') (hTargetDen : swappedTargetDenominator f Aminus Aplus Bminus Bplus = D') (hA : Aminus ≤ Aplus) (hB : Bminus ≤ Bplus) (x : ↥U) :

(quotientEquivSwappedIdentified f Aminus Aplus Bminus Bplus U D U' D' hSourceNum hSourceDen hTargetNum hTargetDen hA hB) (Submodule.Quotient.mk x) = Submodule.Quotient.mk ⟨f ↑x, ⋯⟩