Dimension shifting across a projective middle term #
A short exact sequence 0 ⟶ K ⟶ P ⟶ X ⟶ 0 with projective middle term
induces the natural linear equivalence
Extⁿ⁺¹(K,Y) ≃ Extⁿ⁺²(X,Y).
theorem
MagnitudeConjecture.ProjectiveMiddleDimensionShift.connecting_bijective
{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.Projective S.X₂]
(Y : C)
(n : ℕ)
:
Function.Bijective ⇑(hS.extClass.precompOfLinear k Y ⋯)
The connecting map in positive degree is bijective when the middle term of the short exact sequence is projective.
noncomputable def
MagnitudeConjecture.ProjectiveMiddleDimensionShift.linearEquiv
{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.Projective S.X₂]
(Y : C)
(n : ℕ)
:
CategoryTheory.Abelian.Ext S.X₁ Y (n + 1) ≃ₗ[k] CategoryTheory.Abelian.Ext S.X₃ Y (n + 2)
Dimension shifting, in the variance and normalization used by Auslander's coherent duality.
Instances For
@[simp]
theorem
MagnitudeConjecture.ProjectiveMiddleDimensionShift.linearEquiv_apply
{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.Projective S.X₂]
(Y : C)
(n : ℕ)
(x : CategoryTheory.Abelian.Ext S.X₁ Y (n + 1))
:
(linearEquiv hS Y n) x = hS.extClass.comp x ⋯
theorem
MagnitudeConjecture.ProjectiveMiddleDimensionShift.linearEquiv_postcomp
{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.Projective S.X₂]
{Y Z : C}
(a : Y ⟶ Z)
(n : ℕ)
(x : CategoryTheory.Abelian.Ext S.X₁ Y (n + 1))
:
(linearEquiv hS Z n) (x.comp (CategoryTheory.Abelian.Ext.mk₀ a) ⋯) = ((linearEquiv hS Y n) x).comp (CategoryTheory.Abelian.Ext.mk₀ a) ⋯
Dimension shifting is natural under postcomposition in the second Ext variable.