Idempotent coordinates of quotient modules

def MagnitudeConjecture.RightModule.idempotentCoordinateMap {k A : Type u} [Field k] [Ring A] [Algebra k A] (e : A) {X Y : FinitelyGeneratedCategory A} (f : X ⟶ Y) : ↥(idempotentCoordinate e X) →ₗ[k] ↥(idempotentCoordinate e Y)

A right-module map restricted to the idempotent coordinates.

theorem MagnitudeConjecture.RightModule.idempotentCoordinateMap_surjective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) {X Y : FinitelyGeneratedCategory A} (f : X ⟶ Y) (hf : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) : Function.Surjective ⇑(idempotentCoordinateMap e f)

Surjective module maps remain surjective on an idempotent coordinate.

def MagnitudeConjecture.RightModule.quotientFGMap {A : Type u} [Ring A] (V : FinitelyGeneratedCategory A) (K : Submodule Aᵐᵒᵖ ↑V) : V ⟶ quotientFGObj V K

The canonical quotient morphism in the finite module category.

theorem MagnitudeConjecture.RightModule.coordinateQuotientMap_eq_zero_iff {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) (V : FinitelyGeneratedCategory A) (K : Submodule Aᵐᵒᵖ ↑V) (x : ↥(idempotentCoordinate e V)) : (idempotentCoordinateMap e (quotientFGMap V K)) x = 0 ↔ ↑x ∈ K

Coordinate vectors killed by the quotient are precisely those in K.

theorem MagnitudeConjecture.RightModule.generatedRelations_coordinateMap_ker {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {e : A} (he : IsIdempotentElem e) (hcorner : ∀ (a : Aᵐᵒᵖ), ∃ (c : k), MulOpposite.op e * a * MulOpposite.op e = (algebraMap k Aᵐᵒᵖ) c * MulOpposite.op e) (V : FinitelyGeneratedCategory A) (R : Submodule k ↥(idempotentCoordinate e V)) : (idempotentCoordinateMap e (quotientFGMap V (generatedCoordinateRelations e V R))).ker = R

No additional coordinate relations appear in the quotient by generated relations at a scalar corner.

noncomputable def MagnitudeConjecture.RightModule.generatedRelations_coordinateEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {e : A} (he : IsIdempotentElem e) (hcorner : ∀ (a : Aᵐᵒᵖ), ∃ (c : k), MulOpposite.op e * a * MulOpposite.op e = (algebraMap k Aᵐᵒᵖ) c * MulOpposite.op e) (V : FinitelyGeneratedCategory A) (R : Submodule k ↥(idempotentCoordinate e V)) : (↥(idempotentCoordinate e V) ⧸ R) ≃ₗ[k] ↥(idempotentCoordinate e (quotientFGObj V (generatedCoordinateRelations e V R)))

The quotient by generated relations has coordinate Ve/R.

theorem MagnitudeConjecture.RightModule.generatedRelations_coordinateEquiv_mk {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {e : A} (he : IsIdempotentElem e) (hcorner : ∀ (a : Aᵐᵒᵖ), ∃ (c : k), MulOpposite.op e * a * MulOpposite.op e = (algebraMap k Aᵐᵒᵖ) c * MulOpposite.op e) (V : FinitelyGeneratedCategory A) (R : Submodule k ↥(idempotentCoordinate e V)) (x : ↥(idempotentCoordinate e V)) : (generatedRelations_coordinateEquiv he hcorner V R) (Submodule.Quotient.mk x) = (idempotentCoordinateMap e (quotientFGMap V (generatedCoordinateRelations e V R))) x

The coordinate equivalence sends a vector class to its module quotient class.

noncomputable def MagnitudeConjecture.RightModule.generatedRelations_coordinateEquivTarget {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {e : A} (he : IsIdempotentElem e) (hcorner : ∀ (a : Aᵐᵒᵖ), ∃ (c : k), MulOpposite.op e * a * MulOpposite.op e = (algebraMap k Aᵐᵒᵖ) c * MulOpposite.op e) (V : FinitelyGeneratedCategory A) {W : Type u} [AddCommGroup W] [Module k W] (π : ↥(idempotentCoordinate e V) →ₗ[k] W) (hπ : Function.Surjective ⇑π) : ↥(idempotentCoordinate e (quotientFGObj V (generatedCoordinateRelations e V π.ker))) ≃ₗ[k] W

A surjection π from Ve onto W identifies the coordinate of V/(ker π)A with W.

theorem MagnitudeConjecture.RightModule.generatedRelations_coordinateEquivTarget_map {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {e : A} (he : IsIdempotentElem e) (hcorner : ∀ (a : Aᵐᵒᵖ), ∃ (c : k), MulOpposite.op e * a * MulOpposite.op e = (algebraMap k Aᵐᵒᵖ) c * MulOpposite.op e) (V : FinitelyGeneratedCategory A) {W : Type u} [AddCommGroup W] [Module k W] (π : ↥(idempotentCoordinate e V) →ₗ[k] W) (hπ : Function.Surjective ⇑π) (x : ↥(idempotentCoordinate e V)) : (generatedRelations_coordinateEquivTarget he hcorner V π hπ) ((idempotentCoordinateMap e (quotientFGMap V (generatedCoordinateRelations e V π.ker))) x) = π x

Under the target identification, the coordinate quotient map is exactly π.