Homology

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

DefinitionChen's theorem#

the functor from the stable category of Gorenstein-projective objects of an abelian category to its singularity category is fully faithful.

CategoryTheory.GorensteinProjective.fullyFaithfulToSingularityCategory.{w, v, u} (C : Type u)
  [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] :
  (CategoryTheory.GorensteinProjective.toSingularityCategory C).FullyFaithful
Lean

Formalized in Tau Ceti as CategoryTheory.GorensteinProjective.fullyFaithfulToSingularityCategory.

Other forms

Chen's theorem, faithfulness. Formalized in Tau Ceti as CategoryTheory.GorensteinProjective.instFaithfulProjectiveStableCategoryExactStructureSingularityCategoryToSingularityCategory.

CategoryTheory.GorensteinProjective.instFaithfulProjectiveStableCategoryExactStructureSingularityCategoryToSingularityCategory.{w,
    v, u}
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C]
  [HasDerivedCategory C] : (CategoryTheory.GorensteinProjective.toSingularityCategory C).Faithful

Chen's theorem, fullness. Formalized in Tau Ceti as CategoryTheory.GorensteinProjective.instFullProjectiveStableCategoryExactStructureSingularityCategoryToSingularityCategory.

CategoryTheory.GorensteinProjective.instFullProjectiveStableCategoryExactStructureSingularityCategoryToSingularityCategory.{w,
    v, u}
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C]
  [HasDerivedCategory C] : (CategoryTheory.GorensteinProjective.toSingularityCategory C).Full
Sources
LeanCategoryTheory.GorensteinProjective.fullyFaithfulToSingularityCategory · CategoryTheory.GorensteinProjective.instFaithfulProjectiveStableCategoryExactStructureSingularityCategoryToSingularityCategory · CategoryTheory.GorensteinProjective.instFullProjectiveStableCategoryExactStructureSingularityCategoryToSingularityCategory
Uses 2
Proof usesThe dual Noether isomorphism · The Noether isomorphism for exact categories

TheoremThe comparison theorem (CategoryTheory.Abelian.SpectralObject.isIso_hom_app_abutment_of_isIso_page)#

Let φ : X ⟶ Y be a morphism of spectral objects indexed by EInt and a ≤ b such that H^m(⊥ ≤ i) vanishes for i ≤ a and m ∈ {n, n + 1}, and H^m(i ≤ ⊤) vanishes for i ≥ b and m ∈ {n - 1, n}, for X and Y. If the induced morphism of spectral sequences is an isomorphism on every object of some page r ≥ 2, then φ is an isomorphism on the abutments H^n(⊥ ≤ ⊤).

CategoryTheory.Abelian.SpectralObject.isIso_hom_app_abutment_of_isIso_page.{v_1, u_1} {C : Type u_1}
  [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C]
  {X Y : CategoryTheory.Abelian.SpectralObject C EInt} (φ : X ⟶ Y) {a b : ℤ} (hab : a ≤ b) (n : ℤ)
  (hXa :
    ∀ (m i : ℤ),
      n ≤ m →
        m ≤ n + 1 →
          i ≤ a →
            CategoryTheory.Limits.IsZero
              ((X.H m).obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE ⋯))))
  (hYa :
    ∀ (m i : ℤ),
      n ≤ m →
        m ≤ n + 1 →
          i ≤ a →
            CategoryTheory.Limits.IsZero
              ((Y.H m).obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE ⋯))))
  (hXb :
    ∀ (m i : ℤ),
      n - 1 ≤ m →
        m ≤ n →
          b ≤ i →
            CategoryTheory.Limits.IsZero
              ((X.H m).obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE ⋯))))
  (hYb :
    ∀ (m i : ℤ),
      n - 1 ≤ m →
        m ≤ n →
          b ≤ i →
            CategoryTheory.Limits.IsZero
              ((Y.H m).obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE ⋯))))
  (r : ℤ) (hr : 2 ≤ r)
  (h :
    ∀ (pq : ℤ × ℤ),
      CategoryTheory.IsIso
        (((CategoryTheory.Abelian.SpectralObject.spectralSequenceMap
                  CategoryTheory.Abelian.SpectralObject.coreE₂Cohomological φ).hom
              r hr).f
          pq)) :
  CategoryTheory.IsIso
    ((φ.hom n).app (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE ⋯)))
Lean

Formalized in Tau Ceti as CategoryTheory.Abelian.SpectralObject.isIso_hom_app_abutment_of_isIso_page.

Sources
LeanCategoryTheory.Abelian.SpectralObject.isIso_hom_app_abutment_of_isIso_page
Uses 1 · Used by 2
Proof usesThe comparison theorem on E∞
Used byThe comparison theorem for exhaustive filtrations · The comparison theorem for filtered complexes

TheoremThe comparison theorem for exhaustive filtrations#

Let α be a morphism between the functors of filtrations F of K and G of L, and let n be a degree. Suppose that the stages F_i and G_i at all indices i ≤ a have vanishing cohomology in degrees n and n + 1 (for instance F_a = G_a = ⊥), that in degrees n - 1 and n every element of K and of L lies in some stage of the filtration, and that the graded pieces of both filtrations at all indices i ≥ b have vanishing cohomology. If the morphism of spectral sequences induced by α is an isomorphism on every object of some page r ≥ 2, then α.app ⊤ induces an isomorphism on H^n.

CochainComplex.isIso_homologyMap_of_isIso_spectralSequence_page_of_exhaustive.{v, u_1}
  {R : Type u_1} [Ring R] {K : CochainComplex (ModuleCat R) ℤ} (F : ℤ → CategoryTheory.Subobject K)
  (hF : Monotone F) {L : CochainComplex (ModuleCat R) ℤ} (G : ℤ → CategoryTheory.Subobject L)
  (hG : Monotone G)
  (α : CochainComplex.filtrationFunctor F hF ⟶ CochainComplex.filtrationFunctor G hG) (n : ℤ)
  {a b : ℤ} (hab : a ≤ b)
  (hFa :
    ∀ (m : ℤ),
      n ≤ m →
        m ≤ n + 1 →
          ∀ i ≤ a,
            CategoryTheory.Limits.IsZero
              (HomologicalComplex.homology (CategoryTheory.Subobject.underlying.obj (F i)) m))
  (hGa :
    ∀ (m : ℤ),
      n ≤ m →
        m ≤ n + 1 →
          ∀ i ≤ a,
            CategoryTheory.Limits.IsZero
              (HomologicalComplex.homology (CategoryTheory.Subobject.underlying.obj (G i)) m))
  (hFex :
    ∀ (m : ℤ),
      n - 1 ≤ m → m ≤ n → ∀ (x : ↑(K.X m)), ∃ q, x ∈ (ModuleCat.Hom.hom ((F q).arrow.f m)).range)
  (hGex :
    ∀ (m : ℤ),
      n - 1 ≤ m → m ≤ n → ∀ (x : ↑(L.X m)), ∃ q, x ∈ (ModuleCat.Hom.hom ((G q).arrow.f m)).range)
  (hFb :
    ∀ (m : ℤ),
      n - 1 ≤ m →
        m ≤ n →
          ∀ (i : ℤ),
            b ≤ i →
              CategoryTheory.Limits.IsZero
                (HomologicalComplex.homology
                  (CategoryTheory.Limits.cokernel ((F i).ofLE (F (i + 1)) ⋯)) m))
  (hGb :
    ∀ (m : ℤ),
      n - 1 ≤ m →
        m ≤ n →
          ∀ (i : ℤ),
            b ≤ i →
              CategoryTheory.Limits.IsZero
                (HomologicalComplex.homology
                  (CategoryTheory.Limits.cokernel ((G i).ofLE (G (i + 1)) ⋯)) m))
  (r : ℤ) (hr : 2 ≤ r)
  (h :
    ∀ (pq : ℤ × ℤ),
      CategoryTheory.IsIso
        (((CategoryTheory.Abelian.SpectralObject.spectralSequenceMap
                  CategoryTheory.Abelian.SpectralObject.coreE₂Cohomological
                  (CochainComplex.spectralObjectMap α)).hom
              r hr).f
          pq)) :
  CategoryTheory.IsIso (HomologicalComplex.homologyMap (α.app ⊤) n)
Lean

Formalized in Tau Ceti as CochainComplex.isIso_homologyMap_of_isIso_spectralSequence_page_of_exhaustive.

Sources
LeanCochainComplex.isIso_homologyMap_of_isIso_spectralSequence_page_of_exhaustive
Uses 1
Proof usesThe comparison theorem (CategoryTheory.Abelian.SpectralObject.isIso_hom_app_abutment_of_isIso_page)

TheoremThe comparison theorem for filtered complexes#

Let α be a morphism between the functors of finite increasing filtrations F of K and G of L (F_a = G_a = ⊥ and F_b = G_b = ⊤). If the induced morphism of spectral sequences is an isomorphism on every object of some page r ≥ 2, then α.app ⊤ induces isomorphisms in cohomology.

CochainComplex.isIso_homologyMap_of_isIso_spectralSequence_page.{v_1, u_1} {C : Type u_1}
  [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {K L : CochainComplex C ℤ}
  (F : ℤ → CategoryTheory.Subobject K) (hF : Monotone F) (G : ℤ → CategoryTheory.Subobject L)
  (hG : Monotone G)
  (α : CochainComplex.filtrationFunctor F hF ⟶ CochainComplex.filtrationFunctor G hG) {a b : ℤ}
  (hab : a ≤ b) (hFa : F a = ⊥) (hGa : G a = ⊥) (hFb : F b = ⊤) (hGb : G b = ⊤) (r : ℤ) (hr : 2 ≤ r)
  (h :
    ∀ (pq : ℤ × ℤ),
      CategoryTheory.IsIso
        (((CategoryTheory.Abelian.SpectralObject.spectralSequenceMap
                  CategoryTheory.Abelian.SpectralObject.coreE₂Cohomological
                  (CochainComplex.spectralObjectMap α)).hom
              r hr).f
          pq))
  (n : ℤ) : CategoryTheory.IsIso (HomologicalComplex.homologyMap (α.app ⊤) n)
Lean

Formalized in Tau Ceti as CochainComplex.isIso_homologyMap_of_isIso_spectralSequence_page.

Sources
LeanCochainComplex.isIso_homologyMap_of_isIso_spectralSequence_page
Uses 1
Proof usesThe comparison theorem (CategoryTheory.Abelian.SpectralObject.isIso_hom_app_abutment_of_isIso_page)

TheoremThe comparison theorem on E∞#

Let φ : X ⟶ Y be a morphism of spectral objects indexed by EInt and a ≤ b such that H^n(⊥ ≤ a) and H^n(b ≤ ⊤) vanish for X and Y (the filtrations of the abutments in degree n start at a and end at b). If φ is an isomorphism on EInfty q n for a ≤ q < b, then it is an isomorphism on the abutment H^n(⊥ ≤ ⊤).

CategoryTheory.Abelian.SpectralObject.isIso_hom_app_abutment.{v_1, u_1} {C : Type u_1}
  [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C]
  {X Y : CategoryTheory.Abelian.SpectralObject C EInt} (φ : X ⟶ Y) {a b n : ℤ} (hab : a ≤ b)
  (hXa :
    CategoryTheory.Limits.IsZero
      ((X.H n).obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE ⋯))))
  (hYa :
    CategoryTheory.Limits.IsZero
      ((Y.H n).obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE ⋯))))
  (hXb :
    CategoryTheory.Limits.IsZero
      ((X.H n).obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE ⋯))))
  (hYb :
    CategoryTheory.Limits.IsZero
      ((Y.H n).obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE ⋯))))
  (hE :
    ∀ (q : ℤ),
      a ≤ q →
        q < b →
          CategoryTheory.IsIso
            (CategoryTheory.Abelian.SpectralObject.EMap φ (CategoryTheory.homOfLE ⋯)
              (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE ⋯) (n - 1) n (n + 1) ⋯ ⋯)) :
  CategoryTheory.IsIso
    ((φ.hom n).app (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE ⋯)))
Lean

Formalized in Tau Ceti as CategoryTheory.Abelian.SpectralObject.isIso_hom_app_abutment.

Sources
LeanCategoryTheory.Abelian.SpectralObject.isIso_hom_app_abutment
Used by 1
Used byThe comparison theorem (CategoryTheory.Abelian.SpectralObject.isIso_hom_app_abutment_of_isIso_page)

DefinitionThe differential graded Yoneda lemma#

the Hom complex out of the free rank-one right module is the underlying cochain complex of M.

TauCeti.dgYonedaIso.{uR, uA, uM} {R : Type uR} {A : Type uA} {M : Type (max uA uM)} [CommRing R]
  [Ring A] [Algebra R A] [AddCommGroup M] [_root_.Module R M] [_root_.Module Aᵐᵒᵖ M]
  [IsScalarTower R Aᵐᵒᵖ M] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A}
  {h : TauCeti.IsDGAlgebra 𝒜 d} {ℳ : ℤ → Submodule R M}
  [SetLike.GradedSMul ((TauCeti.InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ]
  [DirectSum.Decomposition ℳ] {dM : M →ₗ[R] M} (hM : TauCeti.IsDGRightModule h ℳ dM) :
  TauCeti.dgRightModuleHomComplex ⋯ hM ≅ TauCeti.gradedCochainComplex ℳ dM ⋯ ⋯
Lean

Formalized in Tau Ceti as TauCeti.dgYonedaIso.

Other forms

The differential graded Yoneda lemma, degreewise. Formalized in Tau Ceti as TauCeti.dgYonedaCochainEquiv.

TauCeti.dgYonedaCochainEquiv.{uR, uA, uM} {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R]
  [Ring A] [Algebra R A] [AddCommGroup M] [_root_.Module R M] [_root_.Module Aᵐᵒᵖ M]
  [IsScalarTower R Aᵐᵒᵖ M] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {ℳ : ℤ → Submodule R M}
  [SetLike.GradedSMul ((TauCeti.InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ] (p : ℤ) :
  ↥(TauCeti.dgRightModuleCochains p) ≃ₗ[R] ↥(ℳ p)

The differential graded Yoneda lemma in degree zero. Formalized in Tau Ceti as TauCeti.dgYonedaHomEquiv.

TauCeti.dgYonedaHomEquiv.{uR, uA, uM} {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R]
  [Ring A] [Algebra R A] [AddCommGroup M] [_root_.Module R M] [_root_.Module Aᵐᵒᵖ M]
  [IsScalarTower R Aᵐᵒᵖ M] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A}
  {h : TauCeti.IsDGAlgebra 𝒜 d} {ℳ : ℤ → Submodule R M}
  [SetLike.GradedSMul ((TauCeti.InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ]
  [DirectSum.Decomposition ℳ] {dM : M →ₗ[R] M} (hM : TauCeti.IsDGRightModule h ℳ dM) :
  TauCeti.DGRightModuleHom ⋯ hM ≃ₗ[R] ↥(hM.cyclesDeg 0)
Sources
LeanTauCeti.dgYonedaIso · TauCeti.dgYonedaCochainEquiv · TauCeti.dgYonedaHomEquiv

TheoremEuler–Poincaré for cubes#

Over a Noetherian ring with the rank-nullity property, such as ℤ or a field, the Euler characteristic of the cohomology of the cube complex of a cube of finite free modules is the sum of the ranks of the vertices F(S), each with the sign (-1) ^ #S. Over ℤ the rank of a cohomology group is the rank of its free part, so torsion does not contribute.

CategoryTheory.Functor.homologyEulerChar_cubeComplex.{w, v, u} {ι : Type w} [Fintype ι]
  [LinearOrder ι] {R : Type u} [Ring R] (F : CategoryTheory.Functor (Finset ι) (ModuleCat R))
  [∀ (S : Finset ι), Module.Free R ↑(F.obj S)] [∀ (S : Finset ι), Module.Finite R ↑(F.obj S)]
  [IsNoetherianRing R] [HasRankNullity.{v, u} R] :
  HomologicalComplex.homologyEulerChar F.cubeComplex =
    ∑ S, ↑(↑S.card).negOnePow * ↑(Module.finrank R ↑(F.obj S))
Lean

Formalized in Tau Ceti as CategoryTheory.Functor.homologyEulerChar_cubeComplex.

Other forms

Euler--Poincaré for a bounded chain complex of vector spaces. Formalized in Tau Ceti as ChainComplex.eulerChar_eq_homologyEulerChar.

ChainComplex.eulerChar_eq_homologyEulerChar.{u, v} {k : Type u} [DivisionRing k]
  (K : ChainComplex (ModuleCat k) ℕ) [∀ (n : ℕ), Module.Finite k ↑(K.X n)]
  (hK : ∀ᶠ (n : ℕ) in Filter.atTop, CategoryTheory.Limits.IsZero (K.X n)) :
  HomologicalComplex.eulerChar K = HomologicalComplex.homologyEulerChar K

Euler--Poincaré for a bounded cochain complex of finitely generated modules. Formalized in Tau Ceti as CochainComplex.eulerChar_eq_homologyEulerChar.

CochainComplex.eulerChar_eq_homologyEulerChar.{u, v} {R : Type u} [Ring R] [IsNoetherianRing R]
  [HasRankNullity.{v, u} R] (K : CochainComplex (ModuleCat R) ℤ)
  (hK : ∀ (n : ℤ), Module.Finite R ↑(K.X n)) (a b : ℤ) [K.IsStrictlyGE a] [K.IsStrictlyLE b] :
  HomologicalComplex.eulerChar K = HomologicalComplex.homologyEulerChar K

Euler--Poincaré for a bounded cochain complex of finitely generated modules. Formalized in Tau Ceti as HomologicalComplex.eulerChar_forgetFG_eq_homologyEulerChar.

HomologicalComplex.eulerChar_forgetFG_eq_homologyEulerChar.{u, v} {R : Type u} [Ring R]
  [IsNoetherianRing R] (K : CochainComplex (FGModuleCat R) ℤ) [HasRankNullity.{v, u} R] (a b : ℤ)
  [K.IsStrictlyGE a] [K.IsStrictlyLE b] :
  (((CategoryTheory.forget₂ (FGModuleCat R) (ModuleCat R)).mapHomologicalComplex
            (ComplexShape.up ℤ)).obj
        K).eulerChar =
    (((CategoryTheory.forget₂ (FGModuleCat R) (ModuleCat R)).mapHomologicalComplex
            (ComplexShape.up ℤ)).obj
        K).homologyEulerChar

Euler--Poincaré for a chain complex of vector spaces indexed by ℕ. Formalized in Tau Ceti as ChainComplex.sum_range_finrank_X_eq_sum_range_finrank_homology.

ChainComplex.sum_range_finrank_X_eq_sum_range_finrank_homology.{u, v} {k : Type u} [DivisionRing k]
  (K : ChainComplex (ModuleCat k) ℕ) {n : ℕ} (hfinite : ∀ i ≤ n, Module.Finite k ↑(K.X i))
  (hn : K.d (n + 1) n = 0) :
  ∑ i ∈ Finset.range (n + 1), (-1) ^ i * ↑(Module.finrank k ↑(K.X i)) =
    ∑ i ∈ Finset.range (n + 1), (-1) ^ i * ↑(Module.finrank k ↑(HomologicalComplex.homology K i))
Sources
LeanCategoryTheory.Functor.homologyEulerChar_cubeComplex · ChainComplex.eulerChar_eq_homologyEulerChar · CochainComplex.eulerChar_eq_homologyEulerChar · HomologicalComplex.eulerChar_forgetFG_eq_homologyEulerChar · ChainComplex.sum_range_finrank_X_eq_sum_range_finrank_homology
Uses 2 · Used by 3
Statement usesCategoryTheory.Functor.cubeComplex
Proof usesThe Euler–Poincaré theorem in abelian K₀
Used byEuler--Poincaré for cellular chains · Euler--Poincaré in one Alexander degree · Euler–Poincaré for Khovanov homology

TheoremGraded Nakayama lemma for free complexes over a polynomial ring#

Let d be a square-zero endomorphism of the free module ι →₀ R[V_v : v ∈ σ] which is homogeneous of degree r when the generator i has degree g i and the variable V_v has negative degree w v, with the degrees g i bounded above. If the reduction d₀ of d modulo the variables, the endomorphism of ι →₀ R with d₀ ∘ ρ = ρ ∘ d for ρ the coordinatewise constant coefficient, is exact, then so is d.

LinearMap.ker_le_range_of_mapRange_constantCoeff.{u_1, u_2, u_3} {R : Type u_1} {σ : Type u_2}
  {ι : Type u_3} [CommRing R] {d₀ : (ι →₀ R) →ₗ[R] ι →₀ R} {w : σ → ℤ} {g : ι → ℤ} {r : ℤ}
  (d : (ι →₀ MvPolynomial σ R) →ₗ[MvPolynomial σ R] ι →₀ MvPolynomial σ R) (hw : ∀ (v : σ), w v < 0)
  (hhom : ∀ (i j : ι), MvPolynomial.IsWeightedHomogeneous w ((d fun₀ | i => 1) j) (g i + r - g j))
  (hd₀ :
    ∀ (x : ι →₀ MvPolynomial σ R),
      d₀ (Finsupp.mapRange ⇑MvPolynomial.constantCoeff ⋯ x) =
        Finsupp.mapRange ⇑MvPolynomial.constantCoeff ⋯ (d x))
  (hg : BddAbove (Set.range g)) (hd : d ∘ₗ d = 0) (hexact : d₀.ker ≤ d₀.range) : d.ker ≤ d.range
Lean

Formalized in Tau Ceti as LinearMap.ker_le_range_of_mapRange_constantCoeff.

Sources
LeanLinearMap.ker_le_range_of_mapRange_constantCoeff
Used by 1
Used byStabilization invariance of GH⁻

TheoremThe Künneth theorem for split complexes#

for complexes K and L of modules over a commutative ring R whose cycles split off their terms and whose homology splits off their cycles, the Künneth map ⨁_{p + q = n} Hₚ(K) ⊗ H_q(L) ⟶ Hₙ(K ⊗ L) is an isomorphism. This applies to complexes of semisimple modules, for instance of vector spaces over a field (HomologicalComplex.isSplitMono_iCycles_of_isSemisimpleModule), and to complexes whose cycles split off and whose homology is projective (HomologicalComplex.isSplitEpi_homologyπ_of_projective).

HomologicalComplex.isIso_homologyKunneth_of_isSplitMono_of_isSplitEpi.{u, u_3} {R : Type u}
  [CommRing R] {I : Type u_3} [Small.{u, u_3} I] [AddMonoid I] {c : ComplexShape I} [c.TensorSigns]
  [DecidableEq I] (K L : HomologicalComplex (ModuleCat R) c) (n : I)
  [∀ (i : I), CategoryTheory.IsSplitMono (K.iCycles i)]
  [∀ (i : I), CategoryTheory.IsSplitEpi (K.homologyπ i)]
  [∀ (i : I), CategoryTheory.IsSplitMono (L.iCycles i)]
  [∀ (i : I), CategoryTheory.IsSplitEpi (L.homologyπ i)] :
  CategoryTheory.IsIso (K.homologyKunneth L n)
Lean

Formalized in Tau Ceti as HomologicalComplex.isIso_homologyKunneth_of_isSplitMono_of_isSplitEpi.

Other forms

The Künneth theorem when one factor has zero differentials and flat terms. Formalized in Tau Ceti as HomologicalComplex.isIso_homologyKunneth_of_d_eq_zero_of_flat.

HomologicalComplex.isIso_homologyKunneth_of_d_eq_zero_of_flat.{u} {R : Type u} [CommRing R]
  (K L : ChainComplex (ModuleCat R) ℕ) [∀ (p : ℕ), Module.Flat R ↑(K.X p)]
  (hK : ∀ (i j : ℕ), K.d i j = 0) (n : ℕ) :
  CategoryTheory.IsIso (HomologicalComplex.homologyKunneth K L n)

The Künneth theorem when the second factor has zero differentials and flat terms. Formalized in Tau Ceti as HomologicalComplex.isIso_homologyKunneth_of_d_eq_zero_of_flat_right.

HomologicalComplex.isIso_homologyKunneth_of_d_eq_zero_of_flat_right.{u} {R : Type u} [CommRing R]
  (K L : ChainComplex (ModuleCat R) ℕ) [∀ (q : ℕ), Module.Flat R ↑(L.X q)]
  (hL : ∀ (i j : ℕ), L.d i j = 0) (n : ℕ) :
  CategoryTheory.IsIso (HomologicalComplex.homologyKunneth K L n)
Sources
LeanHomologicalComplex.isIso_homologyKunneth_of_isSplitMono_of_isSplitEpi · HomologicalComplex.isIso_homologyKunneth_of_d_eq_zero_of_flat · HomologicalComplex.isIso_homologyKunneth_of_d_eq_zero_of_flat_right
Used by 2
Used byThe Künneth short exact sequence over a hereditary commutative ring splits · The Künneth theorem for cubical homology

TheoremThe Morse polynomial identity (ChainComplex.sum_range_monomial_finrank_X_eq)#

If the terms of K through degree n are finite-dimensional and the differential Kₙ₊₁ ⟶ Kₙ vanishes, then in ℕ[X] ∑ᵢ₌₀ⁿ cᵢ Xⁱ = ∑ᵢ₌₀ⁿ bᵢ Xⁱ + (1 + X) Q, where cᵢ is the dimension of Kᵢ, bᵢ that of Hᵢ(K), and Q = ∑ᵢ₌₀ⁿ⁻¹ qᵢ Xⁱ with qᵢ the rank of Kᵢ₊₁ ⟶ Kᵢ: the coefficient of Xⁱ in Q is that rank for i < n and zero otherwise.

ChainComplex.sum_range_monomial_finrank_X_eq.{u, v} {k : Type u} [DivisionRing k]
  (K : ChainComplex (ModuleCat k) ℕ) {n : ℕ} (hfinite : ∀ i ≤ n, Module.Finite k ↑(K.X i))
  (hn : K.d (n + 1) n = 0) :
  ∑ i ∈ Finset.range (n + 1), (Polynomial.monomial i) (Module.finrank k ↑(K.X i)) =
    ∑ i ∈ Finset.range (n + 1),
        (Polynomial.monomial i) (Module.finrank k ↑(HomologicalComplex.homology K i)) +
      (1 + Polynomial.X) *
        ∑ i ∈ Finset.range n,
          (Polynomial.monomial i) (Module.finrank k ↥(ModuleCat.Hom.hom (K.d (i + 1) i)).range)
Lean

Formalized in Tau Ceti as ChainComplex.sum_range_monomial_finrank_X_eq.

Other forms

The Morse polynomial identity from the strong inequalities. Formalized in Tau Ceti as TauCeti.exists_sum_range_monomial_eq_add_mul.

TauCeti.exists_sum_range_monomial_eq_add_mul {b c : ℕ → ℕ} {n : ℕ}
  (hstrong :
    ∀ m < n,
      ∑ i ∈ Finset.range (m + 1), (-1) ^ (m - i) * ↑(b i) ≤
        ∑ i ∈ Finset.range (m + 1), (-1) ^ (m - i) * ↑(c i))
  (heuler :
    ∑ i ∈ Finset.range (n + 1), (-1) ^ i * ↑(b i) = ∑ i ∈ Finset.range (n + 1), (-1) ^ i * ↑(c i)) :
  ∃ Q,
    ∑ i ∈ Finset.range (n + 1), (Polynomial.monomial i) (c i) =
        ∑ i ∈ Finset.range (n + 1), (Polynomial.monomial i) (b i) + (1 + Polynomial.X) * Q ∧
      (∀ i < n,
          ↑(Q.coeff i) =
            ∑ j ∈ Finset.range (i + 1), (-1) ^ (i - j) * ↑(c j) -
              ∑ j ∈ Finset.range (i + 1), (-1) ^ (i - j) * ↑(b j)) ∧
        ∀ (i : ℕ), n ≤ i → Q.coeff i = 0
Sources
LeanChainComplex.sum_range_monomial_finrank_X_eq · TauCeti.exists_sum_range_monomial_eq_add_mul
Uses 1 · Used by 2
Proof usesThe truncated Morse polynomial identity
Used byThe Morse polynomial identity for a CW pair · The Morse polynomial identity (TauCeti.IsMorse.exists_sum_range_monomial_eq_add_mul)

TheoremThe strong Morse inequalities (ChainComplex.sum_range_neg_one_pow_mul_finrank_homology_le)#

If the terms of K through degree n are finite-dimensional, then bₙ - bₙ₋₁ + ⋯ ± b₀ ≤ cₙ - cₙ₋₁ + ⋯ ± c₀, where bᵢ is the dimension of Hᵢ(K) and cᵢ that of Kᵢ. The difference of the two sides is the rank of Kₙ₊₁ ⟶ Kₙ.

ChainComplex.sum_range_neg_one_pow_mul_finrank_homology_le.{u, v} {k : Type u} [DivisionRing k]
  (K : ChainComplex (ModuleCat k) ℕ) (n : ℕ) (hfinite : ∀ i ≤ n, Module.Finite k ↑(K.X i)) :
  ∑ i ∈ Finset.range (n + 1),
      (-1) ^ (n - i) * ↑(Module.finrank k ↑(HomologicalComplex.homology K i)) ≤
    ∑ i ∈ Finset.range (n + 1), (-1) ^ (n - i) * ↑(Module.finrank k ↑(K.X i))
Lean

Formalized in Tau Ceti as ChainComplex.sum_range_neg_one_pow_mul_finrank_homology_le.

Sources
LeanChainComplex.sum_range_neg_one_pow_mul_finrank_homology_le
Used by 1
Used byThe strong Morse inequalities for a CW pair

TheoremThe truncated Morse polynomial identity#

If the terms of K through degree n are finite-dimensional, then in ℕ[X] ∑ᵢ₌₀ⁿ cᵢ Xⁱ + qₙ Xⁿ⁺¹ = ∑ᵢ₌₀ⁿ bᵢ Xⁱ + (1 + X) ∑ᵢ₌₀ⁿ qᵢ Xⁱ, where cᵢ is the dimension of Kᵢ, bᵢ that of Hᵢ(K) and qᵢ the rank of Kᵢ₊₁ ⟶ Kᵢ.

ChainComplex.sum_range_monomial_finrank_X_add_monomial_eq.{u, v} {k : Type u} [DivisionRing k]
  (K : ChainComplex (ModuleCat k) ℕ) (n : ℕ) (hfinite : ∀ i ≤ n, Module.Finite k ↑(K.X i)) :
  ∑ i ∈ Finset.range (n + 1), (Polynomial.monomial i) (Module.finrank k ↑(K.X i)) +
      (Polynomial.monomial (n + 1)) (Module.finrank k ↥(ModuleCat.Hom.hom (K.d (n + 1) n)).range) =
    ∑ i ∈ Finset.range (n + 1),
        (Polynomial.monomial i) (Module.finrank k ↑(HomologicalComplex.homology K i)) +
      (1 + Polynomial.X) *
        ∑ i ∈ Finset.range (n + 1),
          (Polynomial.monomial i) (Module.finrank k ↥(ModuleCat.Hom.hom (K.d (i + 1) i)).range)
Lean

Formalized in Tau Ceti as ChainComplex.sum_range_monomial_finrank_X_add_monomial_eq.

Sources
LeanChainComplex.sum_range_monomial_finrank_X_add_monomial_eq
Used by 1
Used byThe Morse polynomial identity (ChainComplex.sum_range_monomial_finrank_X_eq)

TheoremThe universal coefficient theorem above a projective homology object#

The universal coefficient theorem above a projective homology object, when every object has projective dimension at most one, as for modules over a principal ideal domain: for a chain complex X indexed by ℕ with projective terms whose homology Hₙ(X) is projective, the Kronecker map Hⁿ⁺¹(Hom(X, Y)) →ₗ[k] (Hₙ₊₁(X) ⟶ Y) is bijective, for every object Y. Nothing is assumed about the homology in the other degrees.

TauCeti.ChainComplex.kronecker_bijective_succ_of_projective_homology.{v_1, u_1, u_3} {C : Type u_1}
  [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {k : Type u_3} [CommRing k]
  [CategoryTheory.Linear k C] [∀ (V : C), CategoryTheory.HasProjectiveDimensionLE V 1]
  {X : ChainComplex C ℕ} {Y : C} [∀ (n : ℕ), CategoryTheory.Projective (X.X n)] (n : ℕ)
  [CategoryTheory.Projective (HomologicalComplex.homology X n)] :
  Function.Bijective ⇑(TauCeti.ChainComplex.kronecker k X Y (n + 1))
Lean

Formalized in Tau Ceti as TauCeti.ChainComplex.kronecker_bijective_succ_of_projective_homology.

Sources
LeanTauCeti.ChainComplex.kronecker_bijective_succ_of_projective_homology
Uses 1 · Used by 2
Proof usesThe universal coefficient theorem with projective homology
Used byThe relative universal coefficient theorem above a projective homology module, over a hereditary commutative ring · The universal coefficient theorem above a projective homology module, over a hereditary commutative ring

TheoremThe universal coefficient theorem below the first non-projective homology#

for a chain complex X indexed by ℕ with projective terms whose homology objects are projective below degree n, the Kronecker map Hⁿ(Hom(X, Y)) →ₗ[k] (Hₙ(X) ⟶ Y) is bijective, for every object Y. In particular this holds when X is exact below degree n.

TauCeti.ChainComplex.kronecker_bijective_of_projective_homology_lt.{v_1, u_1, u_3} {C : Type u_1}
  [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {k : Type u_3} [CommRing k]
  [CategoryTheory.Linear k C] {X : ChainComplex C ℕ} {Y : C}
  [∀ (n : ℕ), CategoryTheory.Projective (X.X n)] (n : ℕ)
  (h : ∀ j < n, CategoryTheory.Projective (HomologicalComplex.homology X j)) :
  Function.Bijective ⇑(TauCeti.ChainComplex.kronecker k X Y n)
Informally uses
Lean

Formalized in Tau Ceti as TauCeti.ChainComplex.kronecker_bijective_of_projective_homology_lt.

Sources
LeanTauCeti.ChainComplex.kronecker_bijective_of_projective_homology_lt
Used by 2
Used byThe universal coefficient theorem with projective homology · The relative universal coefficient theorem below the first non-projective homology, over any commutative ring k

TheoremThe universal coefficient theorem with projective homology#

for a chain complex X indexed by ℕ whose terms and homology objects are all projective, the Kronecker map Hⁿ(Hom(X, Y)) →ₗ[k] (Hₙ(X) ⟶ Y) is bijective in every degree, for every object Y.

TauCeti.ChainComplex.kronecker_bijective_of_projective_homology.{v_1, u_1, u_3} {C : Type u_1}
  [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {k : Type u_3} [CommRing k]
  [CategoryTheory.Linear k C] {X : ChainComplex C ℕ} {Y : C}
  [∀ (n : ℕ), CategoryTheory.Projective (X.X n)]
  [∀ (n : ℕ), CategoryTheory.Projective (HomologicalComplex.homology X n)] (n : ℕ) :
  Function.Bijective ⇑(TauCeti.ChainComplex.kronecker k X Y n)
Lean

Formalized in Tau Ceti as TauCeti.ChainComplex.kronecker_bijective_of_projective_homology.

Other forms

The universal coefficient theorem for injective coefficients. Formalized in Tau Ceti as TauCeti.ChainComplex.kronecker_bijective.

TauCeti.ChainComplex.kronecker_bijective.{v_1, u_1, u_2, u_3} {C : Type u_1}
  [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {α : Type u_2}
  [AddRightCancelSemigroup α] [One α] {k : Type u_3} [Ring k] [CategoryTheory.Linear k C]
  {X : ChainComplex C α} {Y : C} [CategoryTheory.Injective Y] (i : α) :
  Function.Bijective ⇑(TauCeti.ChainComplex.kronecker k X Y i)

The universal coefficient theorem in one degree with projective homology below it. Formalized in Tau Ceti as TauCeti.ChainComplex.kronecker_bijective_of_projective_homology_of_add_one_eq.

TauCeti.ChainComplex.kronecker_bijective_of_projective_homology_of_add_one_eq.{v_1, u_1, u_2, u_3}
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {α : Type u_2}
  [AddRightCancelSemigroup α] [One α] {k : Type u_3} [CommRing k] [CategoryTheory.Linear k C]
  {X : ChainComplex C α} {Y : C} {i j : α} (hij : j + 1 = i)
  [CategoryTheory.Projective (HomologicalComplex.cycles X j)]
  [CategoryTheory.IsSplitMono (HomologicalComplex.iCycles X j)]
  [CategoryTheory.IsSplitMono (HomologicalComplex.iCycles X i)]
  [CategoryTheory.Projective (HomologicalComplex.homology X j)] :
  Function.Bijective ⇑(TauCeti.ChainComplex.kronecker k X Y i)
Sources
LeanTauCeti.ChainComplex.kronecker_bijective_of_projective_homology · TauCeti.ChainComplex.kronecker_bijective · TauCeti.ChainComplex.kronecker_bijective_of_projective_homology_of_add_one_eq
Uses 1 · Used by 2
Proof usesThe universal coefficient theorem below the first non-projective homology
Used byThe universal coefficient theorem above a projective homology object · The universal coefficient theorem over a field

TheoremThe weak Morse inequality#

In a homological complex of vector spaces, a homology group has dimension at most that of the finite-dimensional term it is computed from.

HomologicalComplex.finrank_homology_le_finrank_X.{u_1, u_2, u_3} {k : Type u_1} [DivisionRing k]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex (ModuleCat k) c) (i : ι)
  [Module.Finite k ↑(K.X i)] : Module.finrank k ↑(K.homology i) ≤ Module.finrank k ↑(K.X i)
Lean

Formalized in Tau Ceti as HomologicalComplex.finrank_homology_le_finrank_X.

Sources
LeanHomologicalComplex.finrank_homology_le_finrank_X
Used by 1
Used byThe weak Morse inequality for a CW pair

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.