Finite realization of degree-one extension classes

Every degree-one extension class between finitely generated modules over a Noetherian ring is represented by a short exact sequence whose middle term is again finitely generated. The proof constructs the pushout of a finite free presentation explicitly, then compares extension classes after forgetting finite generation.

This is the bounded presentation-theoretic construction needed for the Auslander--Reiten realization argument; it has no dependence on the OP-conjecture formalization.

Explicit pushouts of a presentation

def MagnitudeConjecture.FGExtRealization.PushoutExtension.relationMap {R : Type u} [Ring R] {P S T : Type u} [AddCommGroup P] [AddCommGroup S] [AddCommGroup T] [Module R P] [Module R S] [Module R T] (p : P →ₗ[R] S) (f : ↥p.ker →ₗ[R] T) : ↥p.ker →ₗ[R] T × P

The relation (f x, -x) used to push a kernel presentation out along f.

def MagnitudeConjecture.FGExtRealization.PushoutExtension.relation {R : Type u} [Ring R] {P S T : Type u} [AddCommGroup P] [AddCommGroup S] [AddCommGroup T] [Module R P] [Module R S] [Module R T] (p : P →ₗ[R] S) (f : ↥p.ker →ₗ[R] T) : Submodule R (T × P)

The relation submodule defining the pushout middle term.

@[reducible, inline]

abbrev MagnitudeConjecture.FGExtRealization.PushoutExtension.middle {R : Type u} [Ring R] {P S T : Type u} [AddCommGroup P] [AddCommGroup S] [AddCommGroup T] [Module R P] [Module R S] [Module R T] (p : P →ₗ[R] S) (f : ↥p.ker →ₗ[R] T) : Type u

The explicit pushout middle term.

instance MagnitudeConjecture.FGExtRealization.PushoutExtension.instFiniteMiddle {R : Type u} [Ring R] {P S T : Type u} [AddCommGroup P] [AddCommGroup S] [AddCommGroup T] [Module R P] [Module R S] [Module R T] [Module.Finite R T] [Module.Finite R P] (p : P →ₗ[R] S) (f : ↥p.ker →ₗ[R] T) : Module.Finite R (middle p f)

def MagnitudeConjecture.FGExtRealization.PushoutExtension.inclusion {R : Type u} [Ring R] {P S T : Type u} [AddCommGroup P] [AddCommGroup S] [AddCommGroup T] [Module R P] [Module R S] [Module R T] (p : P →ₗ[R] S) (f : ↥p.ker →ₗ[R] T) : T →ₗ[R] middle p f

The inclusion of the extension kernel into the pushout.

def MagnitudeConjecture.FGExtRealization.PushoutExtension.presentationMap {R : Type u} [Ring R] {P S T : Type u} [AddCommGroup P] [AddCommGroup S] [AddCommGroup T] [Module R P] [Module R S] [Module R T] (p : P →ₗ[R] S) (f : ↥p.ker →ₗ[R] T) : P →ₗ[R] middle p f

The map from the presentation projective into the pushout.

def MagnitudeConjecture.FGExtRealization.PushoutExtension.projection {R : Type u} [Ring R] {P S T : Type u} [AddCommGroup P] [AddCommGroup S] [AddCommGroup T] [Module R P] [Module R S] [Module R T] (p : P →ₗ[R] S) (f : ↥p.ker →ₗ[R] T) : middle p f →ₗ[R] S

The quotient map from the pushout middle term to the presented module.

@[simp]

theorem MagnitudeConjecture.FGExtRealization.PushoutExtension.inclusion_apply {R : Type u} [Ring R] {P S T : Type u} [AddCommGroup P] [AddCommGroup S] [AddCommGroup T] [Module R P] [Module R S] [Module R T] (p : P →ₗ[R] S) (f : ↥p.ker →ₗ[R] T) (t : T) : (inclusion p f) t = (relation p f).mkQ (t, 0)

@[simp]

theorem MagnitudeConjecture.FGExtRealization.PushoutExtension.presentationMap_apply {R : Type u} [Ring R] {P S T : Type u} [AddCommGroup P] [AddCommGroup S] [AddCommGroup T] [Module R P] [Module R S] [Module R T] (p : P →ₗ[R] S) (f : ↥p.ker →ₗ[R] T) (x : P) : (presentationMap p f) x = (relation p f).mkQ (0, x)

@[simp]

theorem MagnitudeConjecture.FGExtRealization.PushoutExtension.projection_mkQ {R : Type u} [Ring R] {P S T : Type u} [AddCommGroup P] [AddCommGroup S] [AddCommGroup T] [Module R P] [Module R S] [Module R T] (p : P →ₗ[R] S) (f : ↥p.ker →ₗ[R] T) (y : T × P) : (projection p f) ((relation p f).mkQ y) = p y.2

theorem MagnitudeConjecture.FGExtRealization.PushoutExtension.inclusion_injective {R : Type u} [Ring R] {P S T : Type u} [AddCommGroup P] [AddCommGroup S] [AddCommGroup T] [Module R P] [Module R S] [Module R T] (p : P →ₗ[R] S) (f : ↥p.ker →ₗ[R] T) : Function.Injective ⇑(inclusion p f)

theorem MagnitudeConjecture.FGExtRealization.PushoutExtension.projection_surjective {R : Type u} [Ring R] {P S T : Type u} [AddCommGroup P] [AddCommGroup S] [AddCommGroup T] [Module R P] [Module R S] [Module R T] (p : P →ₗ[R] S) (hp : Function.Surjective ⇑p) (f : ↥p.ker →ₗ[R] T) : Function.Surjective ⇑(projection p f)

theorem MagnitudeConjecture.FGExtRealization.PushoutExtension.exact_inclusion_projection {R : Type u} [Ring R] {P S T : Type u} [AddCommGroup P] [AddCommGroup S] [AddCommGroup T] [Module R P] [Module R S] [Module R T] (p : P →ₗ[R] S) (f : ↥p.ker →ₗ[R] T) : Function.Exact ⇑(inclusion p f) ⇑(projection p f)

@[reducible, inline]

abbrev MagnitudeConjecture.FGExtRealization.PushoutExtension.shortComplex {R : Type u} [Ring R] {P S T : Type u} [AddCommGroup P] [AddCommGroup S] [AddCommGroup T] [Module R P] [Module R S] [Module R T] (p : P →ₗ[R] S) (f : ↥p.ker →ₗ[R] T) : CategoryTheory.ShortComplex (ModuleCat R)

The explicit pushout short complex in the ambient module category.

theorem MagnitudeConjecture.FGExtRealization.PushoutExtension.shortExact {R : Type u} [Ring R] {P S T : Type u} [AddCommGroup P] [AddCommGroup S] [AddCommGroup T] [Module R P] [Module R S] [Module R T] (p : P →ₗ[R] S) (hp : Function.Surjective ⇑p) (f : ↥p.ker →ₗ[R] T) : (shortComplex p f).ShortExact

theorem MagnitudeConjecture.FGExtRealization.PushoutExtension.presentation_relation {R : Type u} [Ring R] {P S T : Type u} [AddCommGroup P] [AddCommGroup S] [AddCommGroup T] [Module R P] [Module R S] [Module R T] (p : P →ₗ[R] S) (f : ↥p.ker →ₗ[R] T) : inclusion p f ∘ₗ f = presentationMap p f ∘ₗ p.ker.subtype

def MagnitudeConjecture.FGExtRealization.PushoutExtension.fromPresentation {R : Type u} [Ring R] {P S T : Type u} [AddCommGroup P] [AddCommGroup S] [AddCommGroup T] [Module R P] [Module R S] [Module R T] (p : P →ₗ[R] S) (f : ↥p.ker →ₗ[R] T) : p.shortComplexKer ⟶ shortComplex p f

The morphism from the kernel presentation to its explicit pushout.

theorem MagnitudeConjecture.FGExtRealization.PushoutExtension.extClass_eq_precomp {R : Type u} [Ring R] {P S T : Type u} [AddCommGroup P] [AddCommGroup S] [AddCommGroup T] [Module R P] [Module R S] [Module R T] [Small.{u, u} R] (p : P →ₗ[R] S) (hp : Function.Surjective ⇑p) (f : ↥p.ker →ₗ[R] T) : ⋯.extClass = ⋯.extClass.comp (CategoryTheory.Abelian.Ext.mk₀ (ModuleCat.ofHom f)) ⋯

The explicit pushout realizes the connecting image of f.

theorem MagnitudeConjecture.FGExtRealization.PushoutExtension.exists_pushout_with_extClass_eq {R : Type u} [Ring R] {P S T : Type u} [AddCommGroup P] [AddCommGroup S] [AddCommGroup T] [Module R P] [Module R S] [Module R T] [Small.{u, u} R] [Module.Free R P] (p : P →ₗ[R] S) (hp : Function.Surjective ⇑p) (x : CategoryTheory.Abelian.Ext (ModuleCat.of R S) (ModuleCat.of R T) 1) : ∃ (f : ↥p.ker →ₗ[R] T), ⋯.extClass = x

Every ambient Ext¹ class is represented by one of the explicit pushouts.

Bundling the construction in finitely generated modules

@[reducible, inline]

abbrev MagnitudeConjecture.FGExtRealization.inclusion {R : Type u} [Ring R] : CategoryTheory.Functor (FGModuleCat R) (ModuleCat R)

The fully faithful inclusion of finitely generated modules into all modules.

instance MagnitudeConjecture.FGExtRealization.inclusion_additive {R : Type u} [Ring R] : inclusion.Additive

instance MagnitudeConjecture.FGExtRealization.inclusion_preservesProjectiveObjects {R : Type u} [Ring R] [IsNoetherianRing R] : inclusion.PreservesProjectiveObjects

A projective finitely generated module remains projective after forgetting finite generation.

@[reducible, inline]

abbrev MagnitudeConjecture.FGExtRealization.PushoutExtension.fgShortComplex {R : Type u} [Ring R] {P S T : Type u} [AddCommGroup P] [AddCommGroup S] [AddCommGroup T] [Module R P] [Module R S] [Module R T] [Module.Finite R P] [Module.Finite R S] [Module.Finite R T] (p : P →ₗ[R] S) (f : ↥p.ker →ₗ[R] T) : CategoryTheory.ShortComplex (FGModuleCat R)

The explicit pushout sequence bundled in finitely generated modules.

theorem MagnitudeConjecture.FGExtRealization.PushoutExtension.fgShortComplex_map_inclusion {R : Type u} [Ring R] {P S T : Type u} [AddCommGroup P] [AddCommGroup S] [AddCommGroup T] [Module R P] [Module R S] [Module R T] [Module.Finite R P] [Module.Finite R S] [Module.Finite R T] (p : P →ₗ[R] S) (f : ↥p.ker →ₗ[R] T) : (fgShortComplex p f).map FGExtRealization.inclusion = shortComplex p f

theorem MagnitudeConjecture.FGExtRealization.PushoutExtension.fgShortExact {R : Type u} [Ring R] {P S T : Type u} [AddCommGroup P] [AddCommGroup S] [AddCommGroup T] [Module R P] [Module R S] [Module R T] [Module.Finite R P] [Module.Finite R S] [Module.Finite R T] [IsNoetherianRing R] (p : P →ₗ[R] S) (hp : Function.Surjective ⇑p) (f : ↥p.ker →ₗ[R] T) : (fgShortComplex p f).ShortExact

The finite pushout complex is short exact.

theorem MagnitudeConjecture.FGExtRealization.exists_shortExact_with_extClass_eq {R : Type u} [Ring R] [IsNoetherianRing R] [CategoryTheory.HasExt (FGModuleCat R)] (X T : FGModuleCat R) (xi : CategoryTheory.Abelian.Ext X T 1) : ∃ (E : FGModuleCat R) (i : T ⟶ E) (q : E ⟶ X) (zero : CategoryTheory.CategoryStruct.comp i q = 0) (hS : { X₁ := T, X₂ := E, X₃ := X, f := i, g := q, zero := zero }.ShortExact), hS.extClass = xi

Every degree-one Ext class between finitely generated modules is represented by a finite short exact sequence.