Exact

Results named in Tau Ceti's TauCeti.CategoryTheory.Exact modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremThe dual Noether isomorphism#

Given conflations X ⟶ Y ⟶ Z and V ⟶ W ⟶ Y, the pullback Q of W ⟶ Y along X ⟶ Y is at once the kernel of the composite deflation W ⟶ Z and an extension of X by V.

TauCeti.ExactStructure.exists_conflation_comp'.{v, u} {C : Type u}
  [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C]
  (E : TauCeti.ExactStructure C) {X Y Z W V : C} {i : X ⟶ Y} {p : Y ⟶ Z}
  {hip : CategoryTheory.CategoryStruct.comp i p = 0}
  (h₁ : E.Conflation { X₁ := X, X₂ := Y, X₃ := Z, f := i, g := p, zero := hip }) {v : V ⟶ W}
  {q : W ⟶ Y} {hvq : CategoryTheory.CategoryStruct.comp v q = 0}
  (h₂ : E.Conflation { X₁ := V, X₂ := W, X₃ := Y, f := v, g := q, zero := hvq }) :
  ∃ Q c α β,
    ∃ (hc : CategoryTheory.CategoryStruct.comp c (CategoryTheory.CategoryStruct.comp q p) = 0) (hβ :
      CategoryTheory.CategoryStruct.comp β α = 0),
      E.Conflation
          { X₁ := Q, X₂ := W, X₃ := Z, f := c, g := CategoryTheory.CategoryStruct.comp q p,
            zero := hc } ∧
        E.Conflation { X₁ := V, X₂ := Q, X₃ := X, f := β, g := α, zero := hβ } ∧
          CategoryTheory.CategoryStruct.comp c q = CategoryTheory.CategoryStruct.comp α i ∧
            CategoryTheory.CategoryStruct.comp β c = v
Lean

Formalized in Tau Ceti as TauCeti.ExactStructure.exists_conflation_comp'.

Sources
LeanTauCeti.ExactStructure.exists_conflation_comp'
Used by 32
Used byThe general-field Cartan--Poincaré identity · The resolution theorem for modules · The resolution theorem for modules admitting finite resolutions by finitely generated projectives · Cartan-matrix unimodularity · Equivalence invariance of the resolution theorem · TauCeti.gradedCartanEquiv · The Cartan--Poincare identity over a semisimple degree-zero part · The graded Cartan matrix in a projective basis bP and a module basis bM · The graded Cartan matrix of the dual numbers is 1 + q², with ε in degree two, in the bases [A] and [S] · The graded projectives A eᵢ form a basis of K₀^gr(proj A) · The graded quiver q-Euler form at q = 1 is the ungraded Ext-Euler pairing · The graded Ringel formula on Grothendieck classes · The q-Euler matrix of a path algebra is the inverse of its conjugate-transposed graded Cartan matrix · The resolution theorem · The weighted graded Cartan coefficient formula · Chen's theorem · The homotopy category of matrix factorizations is triangulated, with the shift by 1 given by the parity shift · The Euler–Poincaré theorem in abelian K₀ · The graded resolution theorem · The resolution theorem for finite projective resolutions · Modular-Artin reduction of the local Euler characteristic formula · Tate's local Euler characteristic formula · The Euler characteristic formula and G₀ · Artin's identity in G₀(k[G]) over every field, written as induction of the unit from subgroups · Artin's induction identity for every virtual class over every field · Artin's signed permutation identity in the exact Grothendieck group over every field · The Cartan path-count formula · The general-field Cartan/Ext-Euler identity · The modular Artin induction theorem (NSW (7.3.4), Milne ADT I Lemma 2.10) · The modular Artin theorem with multiplier |G| · TauCeti.gradedCartanMatrix_zigzagAlgebra · The action of the graph's Artin group on K₀^gr(proj Z)

DefinitionThe graded comparison theorem#

The comparison map between two finite projective resolutions commutes with the grading shift up to homotopy: the lift of f{1} between the shifted resolutions is homotopic to the shift of the lift of f.

TauCeti.ExactStructure.FiniteResolution.liftShiftHomotopy.{v, u} {C : Type u}
  [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C]
  {E : TauCeti.GradedExactStructure C} {X Y : C} (f : X ⟶ Y)
  (r : E.FiniteResolution E.isProjective X) (r' : E.FiniteResolution E.isProjective Y) :
  Homotopy
    (TauCeti.ExactStructure.FiniteResolution.lift ⋯ (E.shift.functor.map f) r.shiftProjective
      r'.shiftProjective)
    (CategoryTheory.CategoryStruct.comp r.toChainComplexShiftProjectiveIso.hom
      (CategoryTheory.CategoryStruct.comp
        ((E.shift.functor.mapHomologicalComplex (ComplexShape.down ℕ)).map
          (TauCeti.ExactStructure.FiniteResolution.lift ⋯ f r r'))
        r'.toChainComplexShiftProjectiveIso.inv))
Lean

Formalized in Tau Ceti as TauCeti.ExactStructure.FiniteResolution.liftShiftHomotopy.

Sources
LeanTauCeti.ExactStructure.FiniteResolution.liftShiftHomotopy

TheoremThe Noether isomorphism for exact categories#

Given conflations X ⟶ Y ⟶ Z and Y ⟶ W ⟶ V, there is an object Q — the pushout of Y ⟶ W along Y ⟶ Z — which is at once the cokernel of the composite inflation X ⟶ W and an extension of V by Z.

In the classical notation Q ≅ W/X, and the second conflation is Y/X ⟶ W/X ⟶ W/Y. This is Bühler's Lemma 3.5, and it is exactly what an extension-closed subcategory needs in order to inherit axiom E1.

TauCeti.ExactStructure.exists_conflation_comp.{v, u} {C : Type u} [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.Limits.HasBinaryBiproducts C] (E : TauCeti.ExactStructure C) {X Y Z W V : C}
  {i : X ⟶ Y} {p : Y ⟶ Z} {hip : CategoryTheory.CategoryStruct.comp i p = 0}
  (h₁ : E.Conflation { X₁ := X, X₂ := Y, X₃ := Z, f := i, g := p, zero := hip }) {j : Y ⟶ W}
  {v : W ⟶ V} {hjv : CategoryTheory.CategoryStruct.comp j v = 0}
  (h₂ : E.Conflation { X₁ := Y, X₂ := W, X₃ := V, f := j, g := v, zero := hjv }) :
  ∃ Q c α β,
    ∃ (hc : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp i j) c = 0) (hβ :
      CategoryTheory.CategoryStruct.comp α β = 0),
      E.Conflation
          { X₁ := X, X₂ := W, X₃ := Q, f := CategoryTheory.CategoryStruct.comp i j, g := c,
            zero := hc } ∧
        E.Conflation { X₁ := Z, X₂ := Q, X₃ := V, f := α, g := β, zero := hβ } ∧
          CategoryTheory.CategoryStruct.comp j c = CategoryTheory.CategoryStruct.comp p α ∧
            CategoryTheory.CategoryStruct.comp c β = v
Lean

Formalized in Tau Ceti as TauCeti.ExactStructure.exists_conflation_comp.

Sources
LeanTauCeti.ExactStructure.exists_conflation_comp
Used by 33
Used byThe general-field Cartan--Poincaré identity · The resolution theorem for modules · The resolution theorem for modules admitting finite resolutions by finitely generated projectives · Cartan-matrix unimodularity · Equivalence invariance of the resolution theorem · TauCeti.gradedCartanEquiv · The Cartan--Poincare identity over a semisimple degree-zero part · The graded Cartan matrix in a projective basis bP and a module basis bM · The graded Cartan matrix of the dual numbers is 1 + q², with ε in degree two, in the bases [A] and [S] · The graded projectives A eᵢ form a basis of K₀^gr(proj A) · The graded quiver q-Euler form at q = 1 is the ungraded Ext-Euler pairing · The graded Ringel formula on Grothendieck classes · The q-Euler matrix of a path algebra is the inverse of its conjugate-transposed graded Cartan matrix · The resolution theorem · The weighted graded Cartan coefficient formula · Chen's theorem · Happel's theorem · The homotopy category of matrix factorizations is triangulated, with the shift by 1 given by the parity shift · The Euler–Poincaré theorem in abelian K₀ · The graded resolution theorem · The resolution theorem for finite projective resolutions · Modular-Artin reduction of the local Euler characteristic formula · Tate's local Euler characteristic formula · The Euler characteristic formula and G₀ · Artin's identity in G₀(k[G]) over every field, written as induction of the unit from subgroups · Artin's induction identity for every virtual class over every field · Artin's signed permutation identity in the exact Grothendieck group over every field · The Cartan path-count formula · The general-field Cartan/Ext-Euler identity · The modular Artin induction theorem (NSW (7.3.4), Milne ADT I Lemma 2.10) · The modular Artin theorem with multiplier |G| · TauCeti.gradedCartanMatrix_zigzagAlgebra · The action of the graph's Artin group on K₀^gr(proj Z)

TheoremSchanuel's lemma#

Two conflations K ↪ Q ↠ X and K' ↪ Q' ↠ X with projective middle terms have stably isomorphic kernels: K ⊞ Q' ≅ K' ⊞ Q.

Both isomorphisms come from the pullback Q ×_X Q', which base change exhibits at once as an extension of Q' by K and as an extension of Q by K'; projectivity splits both.

TauCeti.ExactStructure.nonempty_iso_biprod_of_projective.{v, u} {C : Type u}
  [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C]
  {E : TauCeti.ExactStructure C} {X K Q : C} {m : K ⟶ Q} {a : Q ⟶ X}
  {hm : CategoryTheory.CategoryStruct.comp m a = 0}
  (hc : E.Conflation { X₁ := K, X₂ := Q, X₃ := X, f := m, g := a, zero := hm })
  (hQ : E.isProjective Q) {K' Q' : C} {m' : K' ⟶ Q'} {a' : Q' ⟶ X}
  {hm' : CategoryTheory.CategoryStruct.comp m' a' = 0}
  (hc' : E.Conflation { X₁ := K', X₂ := Q', X₃ := X, f := m', g := a', zero := hm' })
  (hQ' : E.isProjective Q') : Nonempty (K ⊞ Q' ≅ K' ⊞ Q)
Lean

Formalized in Tau Ceti as TauCeti.ExactStructure.nonempty_iso_biprod_of_projective.

Sources
LeanTauCeti.ExactStructure.nonempty_iso_biprod_of_projective
Used by 1
Used byThe resolution theorem for finite projective resolutions

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.