Degree-one Ext from a short injective presentation

For a short exact sequence 0 ⟶ T ⟶ I ⟶ C ⟶ 0 with injective middle term, this file identifies Ext¹(Y,T) with the quotient of Hom(Y,C) by maps which lift through I. The equivalence is also proved natural under pullback in Y.

This generic routine is adapted from the clean equidistribution formalization. It has no OP-specific dependency.

noncomputable def MagnitudeConjecture.InjectivePresentationExt.connectingLinear {k : Type uk} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (Y : C) : (Y ⟶ S.X₃) →ₗ[k] CategoryTheory.Abelian.Ext Y S.X₁ 1

The connecting map of a short exact sequence, as a linear map.

def MagnitudeConjecture.InjectivePresentationExt.presentationPostcompLinear {k : Type uk} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Linear k C] (S : CategoryTheory.ShortComplex C) (Y : C) : (Y ⟶ S.X₂) →ₗ[k] Y ⟶ S.X₃

Postcomposition with the second map of a short complex.

@[reducible, inline]

abbrev MagnitudeConjecture.InjectivePresentationExt.presentationRange {k : Type uk} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Linear k C] (S : CategoryTheory.ShortComplex C) (Y : C) : Submodule k (Y ⟶ S.X₃)

The presentation coboundaries.

@[simp]

theorem MagnitudeConjecture.InjectivePresentationExt.mem_presentationRange_iff {k : Type uk} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Linear k C] (S : CategoryTheory.ShortComplex C) (Y : C) (f : Y ⟶ S.X₃) : f ∈ presentationRange S Y ↔ ∃ (u : Y ⟶ S.X₂), CategoryTheory.CategoryStruct.comp u S.g = f

theorem MagnitudeConjecture.InjectivePresentationExt.presentationRange_eq_connectingLinear_ker {k : Type uk} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (Y : C) : presentationRange S Y = (connectingLinear hS Y).ker

Exactness identifies presentation coboundaries with the kernel of the connecting map.

theorem MagnitudeConjecture.InjectivePresentationExt.simple_to_cokernel_eq_zero_of_extOne_subsingleton {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {X I S : C} [CategoryTheory.Simple S] (f : X ⟶ I) (hessential : IsEssentialMono f) [Subsingleton (CategoryTheory.Abelian.Ext S X 1)] (t : S ⟶ CategoryTheory.Limits.cokernel f) : t = 0

If X ⟶ I is essential, a simple map to its cokernel must vanish as soon as the corresponding degree-one Ext group is trivial. Exactness first lifts the map to I; essentiality then forces every such simple map to die under the cokernel projection.

theorem MagnitudeConjecture.InjectivePresentationExt.connectingLinear_injective_of_subsingleton_hom_middle {k : Type uk} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (Y : C) [Subsingleton (Y ⟶ S.X₂)] : Function.Injective ⇑(connectingLinear hS Y)

If there are no nonzero maps from Y to the middle term, the connecting map is injective. This is the exact left-hand fragment of the long exact Hom--Ext sequence, packaged for later use without choosing an injective presentation.

theorem MagnitudeConjecture.InjectivePresentationExt.connectingLinear_surjective_of_ext_subsingleton_middle {k : Type uk} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (Y : C) [Subsingleton (CategoryTheory.Abelian.Ext Y S.X₂ 1)] : Function.Surjective ⇑(connectingLinear hS Y)

Vanishing of degree-one extensions into the middle term makes the connecting map surjective.

theorem MagnitudeConjecture.InjectivePresentationExt.connectingLinear_surjective {k : Type uk} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) [CategoryTheory.Injective S.X₂] (Y : C) : Function.Surjective ⇑(connectingLinear hS Y)

Injectivity of the middle term makes the connecting map surjective.

noncomputable def MagnitudeConjecture.InjectivePresentationExt.quotientLinearEquivExtOne {k : Type uk} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) [CategoryTheory.Injective S.X₂] (Y : C) : ((Y ⟶ S.X₃) ⧸ presentationRange S Y) ≃ₗ[k] CategoryTheory.Abelian.Ext Y S.X₁ 1

A short injective presentation computes degree-one Ext.

@[simp]

theorem MagnitudeConjecture.InjectivePresentationExt.quotientLinearEquivExtOne_mk {k : Type uk} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) [CategoryTheory.Injective S.X₂] (Y : C) (f : Y ⟶ S.X₃) : (quotientLinearEquivExtOne hS Y) (Submodule.Quotient.mk f) = (CategoryTheory.Abelian.Ext.mk₀ f).comp hS.extClass ⋯

def MagnitudeConjecture.InjectivePresentationExt.precompQuotient {k : Type uk} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Linear k C] (S : CategoryTheory.ShortComplex C) {Y' Y : C} (a : Y' ⟶ Y) : (Y ⟶ S.X₃) ⧸ presentationRange S Y →ₗ[k] (Y' ⟶ S.X₃) ⧸ presentationRange S Y'

Precomposition descends to the presentation quotient.

@[simp]

theorem MagnitudeConjecture.InjectivePresentationExt.precompQuotient_mk {k : Type uk} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Linear k C] (S : CategoryTheory.ShortComplex C) {Y' Y : C} (a : Y' ⟶ Y) (f : Y ⟶ S.X₃) : (precompQuotient S a) (Submodule.Quotient.mk f) = Submodule.Quotient.mk (CategoryTheory.CategoryStruct.comp a f)

noncomputable def MagnitudeConjecture.InjectivePresentationExt.pullbackLinear {k : Type uk} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] (S : CategoryTheory.ShortComplex C) {Y' Y : C} (a : Y' ⟶ Y) : CategoryTheory.Abelian.Ext Y S.X₁ 1 →ₗ[k] CategoryTheory.Abelian.Ext Y' S.X₁ 1

Pullback on degree-one Ext.

theorem MagnitudeConjecture.InjectivePresentationExt.connectingLinear_precomp {k : Type uk} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) {Y' Y : C} (a : Y' ⟶ Y) (f : Y ⟶ S.X₃) : (connectingLinear hS Y') (CategoryTheory.CategoryStruct.comp a f) = (pullbackLinear S a) ((connectingLinear hS Y) f)

The connecting map commutes with precomposition.

theorem MagnitudeConjecture.InjectivePresentationExt.quotientLinearEquivExtOne_precompQuotient {k : Type uk} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) [CategoryTheory.Injective S.X₂] {Y' Y : C} (a : Y' ⟶ Y) (q : (Y ⟶ S.X₃) ⧸ presentationRange S Y) : (quotientLinearEquivExtOne hS Y') ((precompQuotient S a) q) = (pullbackLinear S a) ((quotientLinearEquivExtOne hS Y) q)

The quotient description is natural under pullback.