Loogle!
Result
Found 2343 declarations mentioning HomologicalComplex. Of these, only the first 200 are shown.
- HomologicalComplex 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (c : ComplexShape ι) : Type (max (max u u_1) v) - HomologicalComplex.instCategory 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} : CategoryTheory.Category.{max u_1 v, max (max u_1 u) v} (HomologicalComplex V c) - HomologicalComplex.X 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (self : HomologicalComplex V c) : ι → V - HomologicalComplex.xNext 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) (i : ι) : V - HomologicalComplex.xPrev 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) (j : ι) : V - HomologicalComplex.zero 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroObject V] : HomologicalComplex V c - HomologicalComplex.instInhabitedOfHasZeroObject 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroObject V] : Inhabited (HomologicalComplex V c) - HomologicalComplex.Hom 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (A B : HomologicalComplex V c) : Type (max u_1 v) - HomologicalComplex.instHasZeroMorphisms 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} : CategoryTheory.Limits.HasZeroMorphisms (HomologicalComplex V c) - HomologicalComplex.id 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (A : HomologicalComplex V c) : A.Hom A - HomologicalComplex.eval 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (c : ComplexShape ι) (i : ι) : CategoryTheory.Functor (HomologicalComplex V c) V - HomologicalComplex.instHasZeroObject 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroObject V] : CategoryTheory.Limits.HasZeroObject (HomologicalComplex V c) - HomologicalComplex.forget 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (c : ComplexShape ι) : CategoryTheory.Functor (HomologicalComplex V c) (CategoryTheory.GradedObject ι V) - HomologicalComplex.instInhabitedHom 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (A B : HomologicalComplex V c) : Inhabited (A.Hom B) - HomologicalComplex.isZero_zero 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroObject V] : CategoryTheory.Limits.IsZero HomologicalComplex.zero - HomologicalComplex.instFaithfulGradedObjectForget 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (c : ComplexShape ι) : (HomologicalComplex.forget V c).Faithful - HomologicalComplex.dFrom 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) (i : ι) : C.X i ⟶ C.xNext i - HomologicalComplex.dTo 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) (j : ι) : C.xPrev j ⟶ C.X j - HomologicalComplex.instPreservesZeroMorphismsEval 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (c : ComplexShape ι) (i : ι) : (HomologicalComplex.eval V c i).PreservesZeroMorphisms - HomologicalComplex.XIsoOfEq 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (K : HomologicalComplex V c) {p q : ι} (h : p = q) : K.X p ≅ K.X q - HomologicalComplex.d 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (self : HomologicalComplex V c) (i j : ι) : self.X i ⟶ self.X j - HomologicalComplex.xNextIso 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) {i j : ι} (r : c.Rel i j) : C.xNext i ≅ C.X j - HomologicalComplex.xPrevIso 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) {i j : ι} (r : c.Rel i j) : C.xPrev j ≅ C.X i - HomologicalComplex.xNextIsoSelf 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) {i : ι} (h : ¬c.Rel i (c.next i)) : C.xNext i ≅ C.X i - HomologicalComplex.xPrevIsoSelf 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) {j : ι} (h : ¬c.Rel (c.prev j) j) : C.xPrev j ≅ C.X j - HomologicalComplex.eval_obj 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (c : ComplexShape ι) (i : ι) (C : HomologicalComplex V c) : (HomologicalComplex.eval V c i).obj C = C.X i - HomologicalComplex.comp 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (A B C : HomologicalComplex V c) (φ : A.Hom B) (ψ : B.Hom C) : A.Hom C - HomologicalComplex.instZeroHom 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (X Y : HomologicalComplex V c) : Zero (X ⟶ Y) - HomologicalComplex.Hom.f 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {A B : HomologicalComplex V c} (self : A.Hom B) (i : ι) : A.X i ⟶ B.X i - HomologicalComplex.Hom.next 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} (f : C₁.Hom C₂) (i : ι) : C₁.xNext i ⟶ C₂.xNext i - HomologicalComplex.Hom.prev 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} (f : C₁.Hom C₂) (j : ι) : C₁.xPrev j ⟶ C₂.xPrev j - HomologicalComplex.forget_obj 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (c : ComplexShape ι) (C : HomologicalComplex V c) (a✝ : ι) : (HomologicalComplex.forget V c).obj C a✝ = C.X a✝ - HomologicalComplex.Hom.isoApp 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} (f : C₁ ≅ C₂) (i : ι) : C₁.X i ≅ C₂.X i - HomologicalComplex.XIsoOfEq_rfl 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (K : HomologicalComplex V c) (p : ι) : K.XIsoOfEq ⋯ = CategoryTheory.Iso.refl (K.X p) - HomologicalComplex.hom_f_injective 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} : Function.Injective fun f => f.f - HomologicalComplex.forgetEval 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (c : ComplexShape ι) (i : ι) : (HomologicalComplex.forget V c).comp (CategoryTheory.GradedObject.eval i) ≅ HomologicalComplex.eval V c i - HomologicalComplex.id_f 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) (i : ι) : (CategoryTheory.CategoryStruct.id C).f i = CategoryTheory.CategoryStruct.id (C.X i) - HomologicalComplex.dNatTrans 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (c : ComplexShape ι) (i j : ι) : HomologicalComplex.eval V c i ⟶ HomologicalComplex.eval V c j - HomologicalComplex.dNatTrans_app 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (c : ComplexShape ι) (i j : ι) (X : HomologicalComplex V c) : (HomologicalComplex.dNatTrans V c i j).app X = X.d i j - HomologicalComplex.Hom.ext 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} {inst✝ : CategoryTheory.Category.{v, u} V} {inst✝¹ : CategoryTheory.Limits.HasZeroMorphisms V} {c : ComplexShape ι} {A B : HomologicalComplex V c} {x y : A.Hom B} (f : x.f = y.f) : x = y - HomologicalComplex.Hom.sqFrom 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} (f : C₁.Hom C₂) (i : ι) : CategoryTheory.Arrow.mk (C₁.dFrom i) ⟶ CategoryTheory.Arrow.mk (C₂.dFrom i) - HomologicalComplex.Hom.sqTo 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} (f : C₁.Hom C₂) (j : ι) : CategoryTheory.Arrow.mk (C₁.dTo j) ⟶ CategoryTheory.Arrow.mk (C₂.dTo j) - HomologicalComplex.Hom.ext_iff 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} {inst✝ : CategoryTheory.Category.{v, u} V} {inst✝¹ : CategoryTheory.Limits.HasZeroMorphisms V} {c : ComplexShape ι} {A B : HomologicalComplex V c} {x y : A.Hom B} : x = y ↔ x.f = y.f - HomologicalComplex.epi_of_epi_f 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {K L : HomologicalComplex V c} (φ : K ⟶ L) (hφ : ∀ (i : ι), CategoryTheory.Epi (φ.f i)) : CategoryTheory.Epi φ - HomologicalComplex.mono_of_mono_f 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {K L : HomologicalComplex V c} (φ : K ⟶ L) (hφ : ∀ (i : ι), CategoryTheory.Mono (φ.f i)) : CategoryTheory.Mono φ - HomologicalComplex.Hom.instIsIsoF 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} (f : C₁ ⟶ C₂) [CategoryTheory.IsIso f] (j : ι) : CategoryTheory.IsIso (f.f j) - HomologicalComplex.Hom.instIsSplitEpiF 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} (f : C₁ ⟶ C₂) [CategoryTheory.IsSplitEpi f] (j : ι) : CategoryTheory.IsSplitEpi (f.f j) - HomologicalComplex.Hom.instIsSplitMonoF 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} (f : C₁ ⟶ C₂) [CategoryTheory.IsSplitMono f] (j : ι) : CategoryTheory.IsSplitMono (f.f j) - HomologicalComplex.Hom.isIso_of_components 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} (f : C₁ ⟶ C₂) [∀ (n : ι), CategoryTheory.IsIso (f.f n)] : CategoryTheory.IsIso f - HomologicalComplex.eval_map 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (c : ComplexShape ι) (i : ι) {X✝ Y✝ : HomologicalComplex V c} (f : X✝ ⟶ Y✝) : (HomologicalComplex.eval V c i).map f = f.f i - HomologicalComplex.forget_map 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (c : ComplexShape ι) {X✝ Y✝ : HomologicalComplex V c} (f : X✝ ⟶ Y✝) (i : ι) : (HomologicalComplex.forget V c).map f i = f.f i - HomologicalComplex.dFrom_comp_xNextIso 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) {i j : ι} (r : c.Rel i j) : CategoryTheory.CategoryStruct.comp (C.dFrom i) (C.xNextIso r).hom = C.d i j - HomologicalComplex.dFrom_eq 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) {i j : ι} (r : c.Rel i j) : C.dFrom i = CategoryTheory.CategoryStruct.comp (C.d i j) (C.xNextIso r).inv - HomologicalComplex.dTo_eq 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) {i j : ι} (r : c.Rel i j) : C.dTo j = CategoryTheory.CategoryStruct.comp (C.xPrevIso r).hom (C.d i j) - HomologicalComplex.xPrevIso_comp_dTo 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) {i j : ι} (r : c.Rel i j) : CategoryTheory.CategoryStruct.comp (C.xPrevIso r).inv (C.dTo j) = C.d i j - HomologicalComplex.XIsoOfEq_hom_comp_d 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (K : HomologicalComplex V c) {p₁ p₂ : ι} (h : p₁ = p₂) (p₃ : ι) : CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h).hom (K.d p₂ p₃) = K.d p₁ p₃ - HomologicalComplex.XIsoOfEq_inv_comp_d 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (K : HomologicalComplex V c) {p₂ p₁ : ι} (h : p₂ = p₁) (p₃ : ι) : CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h).inv (K.d p₂ p₃) = K.d p₁ p₃ - HomologicalComplex.d_comp_XIsoOfEq_hom 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (K : HomologicalComplex V c) {p₂ p₃ : ι} (h : p₂ = p₃) (p₁ : ι) : CategoryTheory.CategoryStruct.comp (K.d p₁ p₂) (K.XIsoOfEq h).hom = K.d p₁ p₃ - HomologicalComplex.d_comp_XIsoOfEq_inv 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (K : HomologicalComplex V c) {p₂ p₃ : ι} (h : p₃ = p₂) (p₁ : ι) : CategoryTheory.CategoryStruct.comp (K.d p₁ p₂) (K.XIsoOfEq h).inv = K.d p₁ p₃ - HomologicalComplex.shape 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (self : HomologicalComplex V c) (i j : ι) : ¬c.Rel i j → self.d i j = 0 - HomologicalComplex.dFrom_eq_zero 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) {i : ι} (h : ¬c.Rel i (c.next i)) : C.dFrom i = 0 - HomologicalComplex.dTo_eq_zero 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) {j : ι} (h : ¬c.Rel (c.prev j) j) : C.dTo j = 0 - HomologicalComplex.ext_of_hom 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} (f : C₁ ⟶ C₂) (h₁ : ∀ (i : ι), C₁.X i = C₂.X i) (h₂ : ∀ (i : ι), f.f i = CategoryTheory.eqToHom ⋯ := by cat_disch) : C₁ = C₂ - HomologicalComplex.ext_of_iso 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} (e : C₁ ≅ C₂) (h₁ : ∀ (i : ι), C₁.X i = C₂.X i) (h₂ : ∀ (i : ι), e.hom.f i = CategoryTheory.eqToHom ⋯ := by cat_disch) : C₁ = C₂ - HomologicalComplex.d_comp_eqToHom 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) {i j j' : ι} (rij : c.Rel i j) (rij' : c.Rel i j') : CategoryTheory.CategoryStruct.comp (C.d i j') (CategoryTheory.eqToHom ⋯) = C.d i j - HomologicalComplex.eqToHom_comp_d 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) {i i' j : ι} (rij : c.Rel i j) (rij' : c.Rel i' j) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (C.d i' j) = C.d i j - HomologicalComplex.eqToHom_f 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} (h : C₁ = C₂) (n : ι) : (CategoryTheory.eqToHom h).f n = CategoryTheory.eqToHom ⋯ - HomologicalComplex.Hom.isoApp_hom 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} (f : C₁ ≅ C₂) (i : ι) : (HomologicalComplex.Hom.isoApp f i).hom = f.hom.f i - HomologicalComplex.Hom.isoApp_inv 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} (f : C₁ ≅ C₂) (i : ι) : (HomologicalComplex.Hom.isoApp f i).inv = f.inv.f i - HomologicalComplex.Hom.sqFrom_id 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C₁ : HomologicalComplex V c) (i : ι) : HomologicalComplex.Hom.sqFrom (CategoryTheory.CategoryStruct.id C₁) i = CategoryTheory.CategoryStruct.id (CategoryTheory.Arrow.mk (C₁.dFrom i)) - HomologicalComplex.Hom.comm_from 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} (f : C₁.Hom C₂) (i : ι) : CategoryTheory.CategoryStruct.comp (f.f i) (C₂.dFrom i) = CategoryTheory.CategoryStruct.comp (C₁.dFrom i) (f.next i) - HomologicalComplex.Hom.comm_to 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} (f : C₁.Hom C₂) (j : ι) : CategoryTheory.CategoryStruct.comp (f.prev j) (C₂.dTo j) = CategoryTheory.CategoryStruct.comp (C₁.dTo j) (f.f j) - HomologicalComplex.Hom.comm 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {A B : HomologicalComplex V c} (f : A.Hom B) (i j : ι) : CategoryTheory.CategoryStruct.comp (f.f i) (B.d i j) = CategoryTheory.CategoryStruct.comp (A.d i j) (f.f j) - HomologicalComplex.image_to_eq_image 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasEqualizers V] {i j : ι} (r : c.Rel i j) : CategoryTheory.Limits.imageSubobject (C.dTo j) = CategoryTheory.Limits.imageSubobject (C.d i j) - HomologicalComplex.dTo_comp_dFrom 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) (j : ι) : CategoryTheory.CategoryStruct.comp (C.dTo j) (C.dFrom j) = 0 - HomologicalComplex.kernel_from_eq_kernel 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) [CategoryTheory.Limits.HasKernels V] {i j : ι} (r : c.Rel i j) : CategoryTheory.Limits.kernelSubobject (C.dFrom i) = CategoryTheory.Limits.kernelSubobject (C.d i j) - HomologicalComplex.congr_hom 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C D : HomologicalComplex V c} {f g : C ⟶ D} (w : f = g) (i : ι) : f.f i = g.f i - HomologicalComplex.hom_ext 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C D : HomologicalComplex V c} (f g : C ⟶ D) (h : ∀ (i : ι), f.f i = g.f i) : f = g - HomologicalComplex.Hom.comm' 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {A B : HomologicalComplex V c} (self : A.Hom B) (i j : ι) : c.Rel i j → CategoryTheory.CategoryStruct.comp (self.f i) (B.d i j) = CategoryTheory.CategoryStruct.comp (A.d i j) (self.f j) - HomologicalComplex.hom_ext_iff 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C D : HomologicalComplex V c} {f g : C ⟶ D} : f = g ↔ ∀ (i : ι), f.f i = g.f i - HomologicalComplex.Hom.inv_f_apply 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} (f : C₁ ⟶ C₂) [CategoryTheory.IsIso f] (j : ι) : (CategoryTheory.inv f).f j = CategoryTheory.inv (f.f j) - HomologicalComplex.d_comp_d 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) (i j k : ι) : CategoryTheory.CategoryStruct.comp (C.d i j) (C.d j k) = 0 - HomologicalComplex.image_eq_image 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasEqualizers V] {i i' j : ι} (r : c.Rel i j) (r' : c.Rel i' j) : CategoryTheory.Limits.imageSubobject (C.d i j) = CategoryTheory.Limits.imageSubobject (C.d i' j) - HomologicalComplex.kernel_eq_kernel 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) [CategoryTheory.Limits.HasKernels V] {i j j' : ι} (r : c.Rel i j) (r' : c.Rel i j') : CategoryTheory.Limits.kernelSubobject (C.d i j) = CategoryTheory.Limits.kernelSubobject (C.d i j') - HomologicalComplex.mk 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (X : ι → V) (d : (i j : ι) → X i ⟶ X j) (shape : ∀ (i j : ι), ¬c.Rel i j → d i j = 0 := by cat_disch) (d_comp_d' : ∀ (i j k : ι), c.Rel i j → c.Rel j k → CategoryTheory.CategoryStruct.comp (d i j) (d j k) = 0 := by cat_disch) : HomologicalComplex V c - HomologicalComplex.Hom.mk 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {A B : HomologicalComplex V c} (f : (i : ι) → A.X i ⟶ B.X i) (comm' : ∀ (i j : ι), c.Rel i j → CategoryTheory.CategoryStruct.comp (f i) (B.d i j) = CategoryTheory.CategoryStruct.comp (A.d i j) (f j) := by cat_disch) : A.Hom B - HomologicalComplex.d_comp_d' 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (self : HomologicalComplex V c) (i j k : ι) : c.Rel i j → c.Rel j k → CategoryTheory.CategoryStruct.comp (self.d i j) (self.d j k) = 0 - HomologicalComplex.dFrom_comp_xNextIso_assoc 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) {i j : ι} (r : c.Rel i j) {Z : V} (h : C.X j ⟶ Z) : CategoryTheory.CategoryStruct.comp (C.dFrom i) (CategoryTheory.CategoryStruct.comp (C.xNextIso r).hom h) = CategoryTheory.CategoryStruct.comp (C.d i j) h - HomologicalComplex.xPrevIso_comp_dTo_assoc 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) {i j : ι} (r : c.Rel i j) {Z : V} (h : C.X j ⟶ Z) : CategoryTheory.CategoryStruct.comp (C.xPrevIso r).inv (CategoryTheory.CategoryStruct.comp (C.dTo j) h) = CategoryTheory.CategoryStruct.comp (C.d i j) h - HomologicalComplex.XIsoOfEq_hom_comp_d_assoc 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (K : HomologicalComplex V c) {p₁ p₂ : ι} (h : p₁ = p₂) (p₃ : ι) {Z : V} (h✝ : K.X p₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h).hom (CategoryTheory.CategoryStruct.comp (K.d p₂ p₃) h✝) = CategoryTheory.CategoryStruct.comp (K.d p₁ p₃) h✝ - HomologicalComplex.XIsoOfEq_inv_comp_d_assoc 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (K : HomologicalComplex V c) {p₂ p₁ : ι} (h : p₂ = p₁) (p₃ : ι) {Z : V} (h✝ : K.X p₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h).inv (CategoryTheory.CategoryStruct.comp (K.d p₂ p₃) h✝) = CategoryTheory.CategoryStruct.comp (K.d p₁ p₃) h✝ - HomologicalComplex.d_comp_XIsoOfEq_hom_assoc 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (K : HomologicalComplex V c) {p₂ p₃ : ι} (h : p₂ = p₃) (p₁ : ι) {Z : V} (h✝ : K.X p₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.d p₁ p₂) (CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h).hom h✝) = CategoryTheory.CategoryStruct.comp (K.d p₁ p₃) h✝ - HomologicalComplex.d_comp_XIsoOfEq_inv_assoc 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (K : HomologicalComplex V c) {p₂ p₃ : ι} (h : p₃ = p₂) (p₁ : ι) {Z : V} (h✝ : K.X p₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.d p₁ p₂) (CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h).inv h✝) = CategoryTheory.CategoryStruct.comp (K.d p₁ p₃) h✝ - HomologicalComplex.XIsoOfEq_hom_comp_XIsoOfEq_hom 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (K : HomologicalComplex V c) {p₁ p₂ p₃ : ι} (h₁₂ : p₁ = p₂) (h₂₃ : p₂ = p₃) : CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h₁₂).hom (K.XIsoOfEq h₂₃).hom = (K.XIsoOfEq ⋯).hom - HomologicalComplex.Hom.sqFrom_left 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} (f : C₁.Hom C₂) (i : ι) : CategoryTheory.Arrow.Hom.left (f.sqFrom i) = f.f i - HomologicalComplex.Hom.sqFrom_right 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} (f : C₁.Hom C₂) (i : ι) : CategoryTheory.Arrow.Hom.right (f.sqFrom i) = f.next i - HomologicalComplex.Hom.sqTo_left 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} (f : C₁.Hom C₂) (j : ι) : CategoryTheory.Arrow.Hom.left (f.sqTo j) = f.prev j - HomologicalComplex.Hom.sqTo_right 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} (f : C₁.Hom C₂) (j : ι) : CategoryTheory.Arrow.Hom.right (f.sqTo j) = f.f j - HomologicalComplex.XIsoOfEq_hom_comp_XIsoOfEq_inv 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (K : HomologicalComplex V c) {p₁ p₂ p₃ : ι} (h₁₂ : p₁ = p₂) (h₃₂ : p₃ = p₂) : CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h₁₂).hom (K.XIsoOfEq h₃₂).inv = (K.XIsoOfEq ⋯).hom - HomologicalComplex.XIsoOfEq_inv_comp_XIsoOfEq_hom 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (K : HomologicalComplex V c) {p₁ p₂ p₃ : ι} (h₂₁ : p₂ = p₁) (h₂₃ : p₂ = p₃) : CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h₂₁).inv (K.XIsoOfEq h₂₃).hom = (K.XIsoOfEq ⋯).hom - HomologicalComplex.XIsoOfEq_inv_comp_XIsoOfEq_inv 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (K : HomologicalComplex V c) {p₁ p₂ p₃ : ι} (h₂₁ : p₂ = p₁) (h₃₂ : p₃ = p₂) : CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h₂₁).inv (K.XIsoOfEq h₃₂).inv = (K.XIsoOfEq ⋯).hom - HomologicalComplex.dFrom_comp_xNextIsoSelf 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) {i : ι} (h : ¬c.Rel i (c.next i)) : CategoryTheory.CategoryStruct.comp (C.dFrom i) (C.xNextIsoSelf h).hom = 0 - HomologicalComplex.xPrevIsoSelf_comp_dTo 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) {j : ι} (h : ¬c.Rel (c.prev j) j) : CategoryTheory.CategoryStruct.comp (C.xPrevIsoSelf h).inv (C.dTo j) = 0 - HomologicalComplex.Hom.comm_from_assoc 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} (f : C₁.Hom C₂) (i : ι) {Z : V} (h : C₂.xNext i ⟶ Z) : CategoryTheory.CategoryStruct.comp (f.f i) (CategoryTheory.CategoryStruct.comp (C₂.dFrom i) h) = CategoryTheory.CategoryStruct.comp (C₁.dFrom i) (CategoryTheory.CategoryStruct.comp (f.next i) h) - HomologicalComplex.Hom.comm_to_assoc 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} (f : C₁.Hom C₂) (j : ι) {Z : V} (h : C₂.X j ⟶ Z) : CategoryTheory.CategoryStruct.comp (f.prev j) (CategoryTheory.CategoryStruct.comp (C₂.dTo j) h) = CategoryTheory.CategoryStruct.comp (C₁.dTo j) (CategoryTheory.CategoryStruct.comp (f.f j) h) - HomologicalComplex.comp_f 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ C₃ : HomologicalComplex V c} (f : C₁ ⟶ C₂) (g : C₂ ⟶ C₃) (i : ι) : (CategoryTheory.CategoryStruct.comp f g).f i = CategoryTheory.CategoryStruct.comp (f.f i) (g.f i) - HomologicalComplex.zero_f 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C D : HomologicalComplex V c) (i : ι) : HomologicalComplex.Hom.f 0 i = 0 - HomologicalComplex.Hom.comm_assoc 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {A B : HomologicalComplex V c} (f : A.Hom B) (i j : ι) {Z : V} (h : B.X j ⟶ Z) : CategoryTheory.CategoryStruct.comp (f.f i) (CategoryTheory.CategoryStruct.comp (B.d i j) h) = CategoryTheory.CategoryStruct.comp (A.d i j) (CategoryTheory.CategoryStruct.comp (f.f j) h) - HomologicalComplex.Hom.next_eq 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} (f : C₁.Hom C₂) {i j : ι} (w : c.Rel i j) : f.next i = CategoryTheory.CategoryStruct.comp (C₁.xNextIso w).hom (CategoryTheory.CategoryStruct.comp (f.f j) (C₂.xNextIso w).inv) - HomologicalComplex.Hom.prev_eq 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} (f : C₁.Hom C₂) {i j : ι} (w : c.Rel i j) : f.prev j = CategoryTheory.CategoryStruct.comp (C₁.xPrevIso w).hom (CategoryTheory.CategoryStruct.comp (f.f i) (C₂.xPrevIso w).inv) - HomologicalComplex.d_comp_d_assoc 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) (i j k : ι) {Z : V} (h : C.X k ⟶ Z) : CategoryTheory.CategoryStruct.comp (C.d i j) (CategoryTheory.CategoryStruct.comp (C.d j k) h) = CategoryTheory.CategoryStruct.comp 0 h - HomologicalComplex.Hom.isoOfComponents 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} (f : (i : ι) → C₁.X i ≅ C₂.X i) (hf : ∀ (i j : ι), c.Rel i j → CategoryTheory.CategoryStruct.comp (f i).hom (C₂.d i j) = CategoryTheory.CategoryStruct.comp (C₁.d i j) (f j).hom := by cat_disch) : C₁ ≅ C₂ - HomologicalComplex.XIsoOfEq_hom_naturality 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {K L : HomologicalComplex V c} (φ : K ⟶ L) {n n' : ι} (h : n = n') : CategoryTheory.CategoryStruct.comp (φ.f n) (L.XIsoOfEq h).hom = CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h).hom (φ.f n') - HomologicalComplex.XIsoOfEq_inv_naturality 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {K L : HomologicalComplex V c} (φ : K ⟶ L) {n n' : ι} (h : n = n') : CategoryTheory.CategoryStruct.comp (φ.f n') (L.XIsoOfEq h).inv = CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h).inv (φ.f n) - HomologicalComplex.XIsoOfEq_hom_comp_XIsoOfEq_hom_assoc 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (K : HomologicalComplex V c) {p₁ p₂ p₃ : ι} (h₁₂ : p₁ = p₂) (h₂₃ : p₂ = p₃) {Z : V} (h : K.X p₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h₁₂).hom (CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h₂₃).hom h) = CategoryTheory.CategoryStruct.comp (K.XIsoOfEq ⋯).hom h - HomologicalComplex.XIsoOfEq_hom_comp_XIsoOfEq_inv_assoc 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (K : HomologicalComplex V c) {p₁ p₂ p₃ : ι} (h₁₂ : p₁ = p₂) (h₃₂ : p₃ = p₂) {Z : V} (h : K.X p₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h₁₂).hom (CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h₃₂).inv h) = CategoryTheory.CategoryStruct.comp (K.XIsoOfEq ⋯).hom h - HomologicalComplex.XIsoOfEq_inv_comp_XIsoOfEq_hom_assoc 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (K : HomologicalComplex V c) {p₁ p₂ p₃ : ι} (h₂₁ : p₂ = p₁) (h₂₃ : p₂ = p₃) {Z : V} (h : K.X p₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h₂₁).inv (CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h₂₃).hom h) = CategoryTheory.CategoryStruct.comp (K.XIsoOfEq ⋯).hom h - HomologicalComplex.XIsoOfEq_inv_comp_XIsoOfEq_inv_assoc 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (K : HomologicalComplex V c) {p₁ p₂ p₃ : ι} (h₂₁ : p₂ = p₁) (h₃₂ : p₃ = p₂) {Z : V} (h : K.X p₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h₂₁).inv (CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h₃₂).inv h) = CategoryTheory.CategoryStruct.comp (K.XIsoOfEq ⋯).hom h - HomologicalComplex.dFrom_comp_xNextIsoSelf_assoc 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) {i : ι} (h : ¬c.Rel i (c.next i)) {Z : V} (h✝ : C.X i ⟶ Z) : CategoryTheory.CategoryStruct.comp (C.dFrom i) (CategoryTheory.CategoryStruct.comp (C.xNextIsoSelf h).hom h✝) = CategoryTheory.CategoryStruct.comp 0 h✝ - HomologicalComplex.xPrevIsoSelf_comp_dTo_assoc 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) {j : ι} (h : ¬c.Rel (c.prev j) j) {Z : V} (h✝ : C.X j ⟶ Z) : CategoryTheory.CategoryStruct.comp (C.xPrevIsoSelf h).inv (CategoryTheory.CategoryStruct.comp (C.dTo j) h✝) = CategoryTheory.CategoryStruct.comp 0 h✝ - HomologicalComplex.Hom.isoOfComponents_app 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} (f : (i : ι) → C₁.X i ≅ C₂.X i) (hf : ∀ (i j : ι), c.Rel i j → CategoryTheory.CategoryStruct.comp (f i).hom (C₂.d i j) = CategoryTheory.CategoryStruct.comp (C₁.d i j) (f j).hom) (i : ι) : HomologicalComplex.Hom.isoApp (HomologicalComplex.Hom.isoOfComponents f hf) i = f i - HomologicalComplex.ext 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} (h_X : C₁.X = C₂.X) (h_d : ∀ (i j : ι), c.Rel i j → CategoryTheory.CategoryStruct.comp (C₁.d i j) (CategoryTheory.eqToHom ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (C₂.d i j)) : C₁ = C₂ - HomologicalComplex.comp_f_assoc 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ C₃ : HomologicalComplex V c} (f : C₁ ⟶ C₂) (g : C₂ ⟶ C₃) (i : ι) {Z : V} (h : C₃.X i ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.CategoryStruct.comp f g).f i) h = CategoryTheory.CategoryStruct.comp (f.f i) (CategoryTheory.CategoryStruct.comp (g.f i) h) - HomologicalComplex.forgetEval_hom_app 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (c : ComplexShape ι) (i : ι) (X : HomologicalComplex V c) : (HomologicalComplex.forgetEval V c i).hom.app X = CategoryTheory.CategoryStruct.id (X.X i) - HomologicalComplex.forgetEval_inv_app 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (c : ComplexShape ι) (i : ι) (X : HomologicalComplex V c) : (HomologicalComplex.forgetEval V c i).inv.app X = CategoryTheory.CategoryStruct.id (X.X i) - HomologicalComplex.XIsoOfEq_hom_naturality_assoc 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {K L : HomologicalComplex V c} (φ : K ⟶ L) {n n' : ι} (h : n = n') {Z : V} (h✝ : L.X n' ⟶ Z) : CategoryTheory.CategoryStruct.comp (φ.f n) (CategoryTheory.CategoryStruct.comp (L.XIsoOfEq h).hom h✝) = CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h).hom (CategoryTheory.CategoryStruct.comp (φ.f n') h✝) - HomologicalComplex.XIsoOfEq_inv_naturality_assoc 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {K L : HomologicalComplex V c} (φ : K ⟶ L) {n n' : ι} (h : n = n') {Z : V} (h✝ : L.X n ⟶ Z) : CategoryTheory.CategoryStruct.comp (φ.f n') (CategoryTheory.CategoryStruct.comp (L.XIsoOfEq h).inv h✝) = CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h).inv (CategoryTheory.CategoryStruct.comp (φ.f n) h✝) - HomologicalComplex.Hom.isoOfComponents_hom_f 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} (f : (i : ι) → C₁.X i ≅ C₂.X i) (hf : ∀ (i j : ι), c.Rel i j → CategoryTheory.CategoryStruct.comp (f i).hom (C₂.d i j) = CategoryTheory.CategoryStruct.comp (C₁.d i j) (f j).hom := by cat_disch) (i : ι) : (HomologicalComplex.Hom.isoOfComponents f hf).hom.f i = (f i).hom - HomologicalComplex.Hom.isoOfComponents_inv_f 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} (f : (i : ι) → C₁.X i ≅ C₂.X i) (hf : ∀ (i j : ι), c.Rel i j → CategoryTheory.CategoryStruct.comp (f i).hom (C₂.d i j) = CategoryTheory.CategoryStruct.comp (C₁.d i j) (f j).hom := by cat_disch) (i : ι) : (HomologicalComplex.Hom.isoOfComponents f hf).inv.f i = (f i).inv - HomologicalComplex.Hom.sqFrom_comp 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ C₃ : HomologicalComplex V c} (f : C₁ ⟶ C₂) (g : C₂ ⟶ C₃) (i : ι) : HomologicalComplex.Hom.sqFrom (CategoryTheory.CategoryStruct.comp f g) i = CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.sqFrom f i) (HomologicalComplex.Hom.sqFrom g i) - HomologicalComplex.Hom.comm_from_apply 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} (f : C₁.Hom C₂) (i : ι) {F : V → V → Type uF} {carrier : V → Type w} {instFunLike : (X Y : V) → FunLike (F X Y) (carrier X) (carrier Y)} [inst : CategoryTheory.ConcreteCategory V F] (x : carrier (C₁.X i)) : (CategoryTheory.ConcreteCategory.hom (C₂.dFrom i)) ((CategoryTheory.ConcreteCategory.hom (f.f i)) x) = (CategoryTheory.ConcreteCategory.hom (f.next i)) ((CategoryTheory.ConcreteCategory.hom (C₁.dFrom i)) x) - HomologicalComplex.Hom.comm_to_apply 📋 Mathlib.Algebra.Homology.HomologicalComplex
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} (f : C₁.Hom C₂) (j : ι) {F : V → V → Type uF} {carrier : V → Type w} {instFunLike : (X Y : V) → FunLike (F X Y) (carrier X) (carrier Y)} [inst : CategoryTheory.ConcreteCategory V F] (x : carrier (C₁.xPrev j)) : (CategoryTheory.ConcreteCategory.hom (C₂.dTo j)) ((CategoryTheory.ConcreteCategory.hom (f.prev j)) x) = (CategoryTheory.ConcreteCategory.hom (f.f j)) ((CategoryTheory.ConcreteCategory.hom (C₁.dTo j)) x) - HomologicalComplex.single 📋 Mathlib.Algebra.Homology.Single
(V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) : CategoryTheory.Functor V (HomologicalComplex V c) - HomologicalComplex.instFaithfulSingle 📋 Mathlib.Algebra.Homology.Single
{V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] {c : ComplexShape ι} (j : ι) : (HomologicalComplex.single V c j).Faithful - HomologicalComplex.instFullSingle 📋 Mathlib.Algebra.Homology.Single
{V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] {c : ComplexShape ι} (j : ι) : (HomologicalComplex.single V c j).Full - HomologicalComplex.instPreservesZeroMorphismsSingle 📋 Mathlib.Algebra.Homology.Single
{V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] {c : ComplexShape ι} (j : ι) : (HomologicalComplex.single V c j).PreservesZeroMorphisms - HomologicalComplex.single_obj_X_self 📋 Mathlib.Algebra.Homology.Single
{V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) (A : V) : ((HomologicalComplex.single V c j).obj A).X j = A - HomologicalComplex.singleObjXSelf 📋 Mathlib.Algebra.Homology.Single
{V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) (A : V) : ((HomologicalComplex.single V c j).obj A).X j ≅ A - HomologicalComplex.isZero_single_obj_X 📋 Mathlib.Algebra.Homology.Single
{V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) (A : V) (i : ι) (hi : i ≠ j) : CategoryTheory.Limits.IsZero (((HomologicalComplex.single V c j).obj A).X i) - HomologicalComplex.singleObjXIsoOfEq 📋 Mathlib.Algebra.Homology.Single
{V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) (A : V) (i : ι) (hi : i = j) : ((HomologicalComplex.single V c j).obj A).X i ≅ A - HomologicalComplex.singleCompEvalIsoSelf 📋 Mathlib.Algebra.Homology.Single
(V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) : (HomologicalComplex.single V c j).comp (HomologicalComplex.eval V c j) ≅ CategoryTheory.Functor.id V - HomologicalComplex.isZero_single_comp_eval 📋 Mathlib.Algebra.Homology.Single
(V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j i : ι) (hi : i ≠ j) : CategoryTheory.Limits.IsZero ((HomologicalComplex.single V c j).comp (HomologicalComplex.eval V c i)) - HomologicalComplex.mkHomFromSingle 📋 Mathlib.Algebra.Homology.Single
{V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] {c : ComplexShape ι} {K : HomologicalComplex V c} {j : ι} {A : V} (φ : A ⟶ K.X j) (hφ : ∀ (k : ι), c.Rel j k → CategoryTheory.CategoryStruct.comp φ (K.d j k) = 0) : (HomologicalComplex.single V c j).obj A ⟶ K - HomologicalComplex.mkHomToSingle 📋 Mathlib.Algebra.Homology.Single
{V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] {c : ComplexShape ι} {K : HomologicalComplex V c} {j : ι} {A : V} (φ : K.X j ⟶ A) (hφ : ∀ (i : ι), c.Rel i j → CategoryTheory.CategoryStruct.comp (K.d i j) φ = 0) : K ⟶ (HomologicalComplex.single V c j).obj A - HomologicalComplex.singleCompEvalIsoSelf_hom_app 📋 Mathlib.Algebra.Homology.Single
(V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) (X : V) : (HomologicalComplex.singleCompEvalIsoSelf V c j).hom.app X = (HomologicalComplex.singleObjXSelf c j X).hom - HomologicalComplex.singleCompEvalIsoSelf_inv_app 📋 Mathlib.Algebra.Homology.Single
(V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) (X : V) : (HomologicalComplex.singleCompEvalIsoSelf V c j).inv.app X = (HomologicalComplex.singleObjXSelf c j X).inv - ChainComplex.single₀ObjXSelf 📋 Mathlib.Algebra.Homology.Single
{V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] (X : V) : HomologicalComplex.singleObjXSelf (ComplexShape.down ℕ) 0 X = CategoryTheory.Iso.refl (((HomologicalComplex.single V (ComplexShape.down ℕ) 0).obj X).X 0) - CochainComplex.single₀ObjXSelf 📋 Mathlib.Algebra.Homology.Single
{V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] (X : V) : HomologicalComplex.singleObjXSelf (ComplexShape.up ℕ) 0 X = CategoryTheory.Iso.refl (((HomologicalComplex.single V (ComplexShape.up ℕ) 0).obj X).X 0) - HomologicalComplex.from_single_hom_ext 📋 Mathlib.Algebra.Homology.Single
{V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] {c : ComplexShape ι} {K : HomologicalComplex V c} {j : ι} {A : V} {f g : (HomologicalComplex.single V c j).obj A ⟶ K} (hfg : f.f j = g.f j) : f = g - HomologicalComplex.to_single_hom_ext 📋 Mathlib.Algebra.Homology.Single
{V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] {c : ComplexShape ι} {K : HomologicalComplex V c} {j : ι} {A : V} {f g : K ⟶ (HomologicalComplex.single V c j).obj A} (hfg : f.f j = g.f j) : f = g - HomologicalComplex.from_single_hom_ext_iff 📋 Mathlib.Algebra.Homology.Single
{V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] {c : ComplexShape ι} {K : HomologicalComplex V c} {j : ι} {A : V} {f g : (HomologicalComplex.single V c j).obj A ⟶ K} : f = g ↔ f.f j = g.f j - HomologicalComplex.to_single_hom_ext_iff 📋 Mathlib.Algebra.Homology.Single
{V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] {c : ComplexShape ι} {K : HomologicalComplex V c} {j : ι} {A : V} {f g : K ⟶ (HomologicalComplex.single V c j).obj A} : f = g ↔ f.f j = g.f j - HomologicalComplex.mkHomFromSingle_f 📋 Mathlib.Algebra.Homology.Single
{V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] {c : ComplexShape ι} {K : HomologicalComplex V c} {j : ι} {A : V} (φ : A ⟶ K.X j) (hφ : ∀ (k : ι), c.Rel j k → CategoryTheory.CategoryStruct.comp φ (K.d j k) = 0) : (HomologicalComplex.mkHomFromSingle φ hφ).f j = CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjXSelf c j A).hom φ - HomologicalComplex.mkHomToSingle_f 📋 Mathlib.Algebra.Homology.Single
{V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] {c : ComplexShape ι} {K : HomologicalComplex V c} {j : ι} {A : V} (φ : K.X j ⟶ A) (hφ : ∀ (i : ι), c.Rel i j → CategoryTheory.CategoryStruct.comp (K.d i j) φ = 0) : (HomologicalComplex.mkHomToSingle φ hφ).f j = CategoryTheory.CategoryStruct.comp φ (HomologicalComplex.singleObjXSelf c j A).inv - HomologicalComplex.single_obj_d 📋 Mathlib.Algebra.Homology.Single
{V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) (A : V) (k l : ι) : ((HomologicalComplex.single V c j).obj A).d k l = 0 - HomologicalComplex.single_map_f_self 📋 Mathlib.Algebra.Homology.Single
{V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) {A B : V} (f : A ⟶ B) : ((HomologicalComplex.single V c j).map f).f j = CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjXSelf c j A).hom (CategoryTheory.CategoryStruct.comp f (HomologicalComplex.singleObjXSelf c j B).inv) - HomologicalComplex.single_map_f_self_assoc 📋 Mathlib.Algebra.Homology.Single
{V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) {A B : V} (f : A ⟶ B) {Z : V} (h : ((HomologicalComplex.single V c j).obj B).X j ⟶ Z) : CategoryTheory.CategoryStruct.comp (((HomologicalComplex.single V c j).map f).f j) h = CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjXSelf c j A).hom (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjXSelf c j B).inv h)) - HomologicalComplex.instPreadditive 📋 Mathlib.Algebra.Homology.Additive
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} : CategoryTheory.Preadditive (HomologicalComplex V c) - HomologicalComplex.eval_additive 📋 Mathlib.Algebra.Homology.Additive
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} (i : ι) : (HomologicalComplex.eval V c i).Additive - CategoryTheory.Functor.mapHomologicalComplex 📋 Mathlib.Algebra.Homology.Additive
{ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [CategoryTheory.Category.{v_2, u_3} W₁] [CategoryTheory.Category.{v_3, u_4} W₂] [CategoryTheory.Limits.HasZeroMorphisms W₁] [CategoryTheory.Limits.HasZeroMorphisms W₂] (F : CategoryTheory.Functor W₁ W₂) [F.PreservesZeroMorphisms] (c : ComplexShape ι) : CategoryTheory.Functor (HomologicalComplex W₁ c) (HomologicalComplex W₂ c) - HomologicalComplex.instAdditiveSingle 📋 Mathlib.Algebra.Homology.Additive
{ι : Type u_1} {c : ComplexShape ι} (W : Type u_6) [CategoryTheory.Category.{v_5, u_6} W] [CategoryTheory.Preadditive W] [CategoryTheory.Limits.HasZeroObject W] [DecidableEq ι] (j : ι) : (HomologicalComplex.single W c j).Additive - CategoryTheory.Equivalence.mapHomologicalComplex 📋 Mathlib.Algebra.Homology.Additive
{ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [CategoryTheory.Category.{v_2, u_3} W₁] [CategoryTheory.Category.{v_3, u_4} W₂] [CategoryTheory.Limits.HasZeroMorphisms W₁] [CategoryTheory.Limits.HasZeroMorphisms W₂] (e : W₁ ≌ W₂) [e.functor.PreservesZeroMorphisms] (c : ComplexShape ι) : HomologicalComplex W₁ c ≌ HomologicalComplex W₂ c - HomologicalComplex.instAddCommGroupHom 📋 Mathlib.Algebra.Homology.Additive
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} : AddCommGroup (C ⟶ D) - HomologicalComplex.instAddHom 📋 Mathlib.Algebra.Homology.Additive
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} : Add (C ⟶ D) - HomologicalComplex.instNegHom 📋 Mathlib.Algebra.Homology.Additive
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} : Neg (C ⟶ D) - HomologicalComplex.instSubHom 📋 Mathlib.Algebra.Homology.Additive
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} : Sub (C ⟶ D) - HomologicalComplex.instZeroHom_1 📋 Mathlib.Algebra.Homology.Additive
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} : Zero (C ⟶ D) - HomologicalComplex.hasIntScalar 📋 Mathlib.Algebra.Homology.Additive
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} : SMul ℤ (C ⟶ D) - HomologicalComplex.hasNatScalar 📋 Mathlib.Algebra.Homology.Additive
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} : SMul ℕ (C ⟶ D) - CategoryTheory.Functor.mapHomologicalComplex_reflects_iso 📋 Mathlib.Algebra.Homology.Additive
{ι : Type u_1} (W₁ : Type u_3) {W₂ : Type u_4} [CategoryTheory.Category.{v_2, u_3} W₁] [CategoryTheory.Category.{v_3, u_4} W₂] [CategoryTheory.Limits.HasZeroMorphisms W₁] [CategoryTheory.Limits.HasZeroMorphisms W₂] (F : CategoryTheory.Functor W₁ W₂) [F.PreservesZeroMorphisms] [F.ReflectsIsomorphisms] (c : ComplexShape ι) : (F.mapHomologicalComplex c).ReflectsIsomorphisms - CategoryTheory.instPreservesZeroMorphismsHomologicalComplexMapHomologicalComplex 📋 Mathlib.Algebra.Homology.Additive
{ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [CategoryTheory.Category.{v_2, u_3} W₁] [CategoryTheory.Category.{v_3, u_4} W₂] [CategoryTheory.Limits.HasZeroMorphisms W₁] [CategoryTheory.Limits.HasZeroMorphisms W₂] (F : CategoryTheory.Functor W₁ W₂) [F.PreservesZeroMorphisms] (c : ComplexShape ι) : (F.mapHomologicalComplex c).PreservesZeroMorphisms - CategoryTheory.Functor.mapHomologicalComplex_obj_X 📋 Mathlib.Algebra.Homology.Additive
{ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [CategoryTheory.Category.{v_2, u_3} W₁] [CategoryTheory.Category.{v_3, u_4} W₂] [CategoryTheory.Limits.HasZeroMorphisms W₁] [CategoryTheory.Limits.HasZeroMorphisms W₂] (F : CategoryTheory.Functor W₁ W₂) [F.PreservesZeroMorphisms] (c : ComplexShape ι) (C : HomologicalComplex W₁ c) (i : ι) : ((F.mapHomologicalComplex c).obj C).X i = F.obj (C.X i) - CategoryTheory.instFaithfulHomologicalComplexMapHomologicalComplex 📋 Mathlib.Algebra.Homology.Additive
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {W : Type u_2} [CategoryTheory.Category.{v_1, u_2} W] [CategoryTheory.Preadditive W] (F : CategoryTheory.Functor V W) [F.Additive] (c : ComplexShape ι) [F.Faithful] : (F.mapHomologicalComplex c).Faithful - CategoryTheory.Functor.mapHomologicalComplexIdIso 📋 Mathlib.Algebra.Homology.Additive
{ι : Type u_1} (W₁ : Type u_3) [CategoryTheory.Category.{v_2, u_3} W₁] [CategoryTheory.Limits.HasZeroMorphisms W₁] (c : ComplexShape ι) : (CategoryTheory.Functor.id W₁).mapHomologicalComplex c ≅ CategoryTheory.Functor.id (HomologicalComplex W₁ c) - CategoryTheory.instFullHomologicalComplexMapHomologicalComplexOfFaithful 📋 Mathlib.Algebra.Homology.Additive
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {W : Type u_2} [CategoryTheory.Category.{v_1, u_2} W] [CategoryTheory.Preadditive W] (F : CategoryTheory.Functor V W) [F.Additive] (c : ComplexShape ι) [F.Faithful] [F.Full] : (F.mapHomologicalComplex c).Full - CategoryTheory.Functor.map_homogical_complex_additive 📋 Mathlib.Algebra.Homology.Additive
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {W : Type u_2} [CategoryTheory.Category.{v_1, u_2} W] [CategoryTheory.Preadditive W] (F : CategoryTheory.Functor V W) [F.Additive] (c : ComplexShape ι) : (F.mapHomologicalComplex c).Additive - CategoryTheory.Equivalence.mapHomologicalComplex_functor 📋 Mathlib.Algebra.Homology.Additive
{ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [CategoryTheory.Category.{v_2, u_3} W₁] [CategoryTheory.Category.{v_3, u_4} W₂] [CategoryTheory.Limits.HasZeroMorphisms W₁] [CategoryTheory.Limits.HasZeroMorphisms W₂] (e : W₁ ≌ W₂) [e.functor.PreservesZeroMorphisms] (c : ComplexShape ι) : (e.mapHomologicalComplex c).functor = e.functor.mapHomologicalComplex c - CategoryTheory.Equivalence.mapHomologicalComplex_inverse 📋 Mathlib.Algebra.Homology.Additive
{ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [CategoryTheory.Category.{v_2, u_3} W₁] [CategoryTheory.Category.{v_3, u_4} W₂] [CategoryTheory.Limits.HasZeroMorphisms W₁] [CategoryTheory.Limits.HasZeroMorphisms W₂] (e : W₁ ≌ W₂) [e.functor.PreservesZeroMorphisms] (c : ComplexShape ι) : (e.mapHomologicalComplex c).inverse = e.inverse.mapHomologicalComplex c - CategoryTheory.NatIso.mapHomologicalComplex 📋 Mathlib.Algebra.Homology.Additive
{ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [CategoryTheory.Category.{v_2, u_3} W₁] [CategoryTheory.Category.{v_3, u_4} W₂] [CategoryTheory.Limits.HasZeroMorphisms W₁] [CategoryTheory.Limits.HasZeroMorphisms W₂] {F G : CategoryTheory.Functor W₁ W₂} [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] (α : F ≅ G) (c : ComplexShape ι) : F.mapHomologicalComplex c ≅ G.mapHomologicalComplex c - HomologicalComplex.singleMapHomologicalComplex 📋 Mathlib.Algebra.Homology.Additive
{ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [CategoryTheory.Category.{v_2, u_3} W₁] [CategoryTheory.Category.{v_3, u_4} W₂] [CategoryTheory.Limits.HasZeroMorphisms W₁] [CategoryTheory.Limits.HasZeroMorphisms W₂] [CategoryTheory.Limits.HasZeroObject W₁] [CategoryTheory.Limits.HasZeroObject W₂] (F : CategoryTheory.Functor W₁ W₂) [F.PreservesZeroMorphisms] (c : ComplexShape ι) [DecidableEq ι] (j : ι) : (HomologicalComplex.single W₁ c j).comp (F.mapHomologicalComplex c) ≅ F.comp (HomologicalComplex.single W₂ c j) - CategoryTheory.Functor.mapHomologicalComplex_obj_d 📋 Mathlib.Algebra.Homology.Additive
{ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [CategoryTheory.Category.{v_2, u_3} W₁] [CategoryTheory.Category.{v_3, u_4} W₂] [CategoryTheory.Limits.HasZeroMorphisms W₁] [CategoryTheory.Limits.HasZeroMorphisms W₂] (F : CategoryTheory.Functor W₁ W₂) [F.PreservesZeroMorphisms] (c : ComplexShape ι) (C : HomologicalComplex W₁ c) (i j : ι) : ((F.mapHomologicalComplex c).obj C).d i j = F.map (C.d i j) - CategoryTheory.NatTrans.mapHomologicalComplex 📋 Mathlib.Algebra.Homology.Additive
{ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [CategoryTheory.Category.{v_2, u_3} W₁] [CategoryTheory.Category.{v_3, u_4} W₂] [CategoryTheory.Limits.HasZeroMorphisms W₁] [CategoryTheory.Limits.HasZeroMorphisms W₂] {F G : CategoryTheory.Functor W₁ W₂} [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] (α : F ⟶ G) (c : ComplexShape ι) : F.mapHomologicalComplex c ⟶ G.mapHomologicalComplex c - CategoryTheory.Functor.mapHomologicalComplexCompIso 📋 Mathlib.Algebra.Homology.Additive
{ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} {W₃ : Type u_5} [CategoryTheory.Category.{v_2, u_3} W₁] [CategoryTheory.Category.{v_3, u_4} W₂] [CategoryTheory.Category.{v_4, u_5} W₃] [CategoryTheory.Limits.HasZeroMorphisms W₁] [CategoryTheory.Limits.HasZeroMorphisms W₂] [CategoryTheory.Limits.HasZeroMorphisms W₃] {F : CategoryTheory.Functor W₁ W₂} {G : CategoryTheory.Functor W₂ W₃} {H : CategoryTheory.Functor W₁ W₃} (e : F.comp G ≅ H) [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] [H.PreservesZeroMorphisms] (c : ComplexShape ι) : (F.mapHomologicalComplex c).comp (G.mapHomologicalComplex c) ≅ H.mapHomologicalComplex c - HomologicalComplex.zero_f_apply 📋 Mathlib.Algebra.Homology.Additive
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} (i : ι) : HomologicalComplex.Hom.f 0 i = 0 - CategoryTheory.NatTrans.mapHomologicalComplex_app_f 📋 Mathlib.Algebra.Homology.Additive
{ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [CategoryTheory.Category.{v_2, u_3} W₁] [CategoryTheory.Category.{v_3, u_4} W₂] [CategoryTheory.Limits.HasZeroMorphisms W₁] [CategoryTheory.Limits.HasZeroMorphisms W₂] {F G : CategoryTheory.Functor W₁ W₂} [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] (α : F ⟶ G) (c : ComplexShape ι) (C : HomologicalComplex W₁ c) (x✝ : ι) : ((CategoryTheory.NatTrans.mapHomologicalComplex α c).app C).f x✝ = α.app (C.X x✝) - CategoryTheory.NatTrans.mapHomologicalComplex_id 📋 Mathlib.Algebra.Homology.Additive
{ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [CategoryTheory.Category.{v_2, u_3} W₁] [CategoryTheory.Category.{v_3, u_4} W₂] [CategoryTheory.Limits.HasZeroMorphisms W₁] [CategoryTheory.Limits.HasZeroMorphisms W₂] (c : ComplexShape ι) (F : CategoryTheory.Functor W₁ W₂) [F.PreservesZeroMorphisms] : CategoryTheory.NatTrans.mapHomologicalComplex (CategoryTheory.CategoryStruct.id F) c = CategoryTheory.CategoryStruct.id (F.mapHomologicalComplex c) - CategoryTheory.NatIso.mapHomologicalComplex_hom_app_f 📋 Mathlib.Algebra.Homology.Additive
{ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [CategoryTheory.Category.{v_2, u_3} W₁] [CategoryTheory.Category.{v_3, u_4} W₂] [CategoryTheory.Limits.HasZeroMorphisms W₁] [CategoryTheory.Limits.HasZeroMorphisms W₂] {F G : CategoryTheory.Functor W₁ W₂} [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] (α : F ≅ G) (c : ComplexShape ι) (C : HomologicalComplex W₁ c) (x✝ : ι) : ((CategoryTheory.NatIso.mapHomologicalComplex α c).hom.app C).f x✝ = α.hom.app (C.X x✝) - CategoryTheory.NatIso.mapHomologicalComplex_inv_app_f 📋 Mathlib.Algebra.Homology.Additive
{ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [CategoryTheory.Category.{v_2, u_3} W₁] [CategoryTheory.Category.{v_3, u_4} W₂] [CategoryTheory.Limits.HasZeroMorphisms W₁] [CategoryTheory.Limits.HasZeroMorphisms W₂] {F G : CategoryTheory.Functor W₁ W₂} [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] (α : F ≅ G) (c : ComplexShape ι) (C : HomologicalComplex W₁ c) (x✝ : ι) : ((CategoryTheory.NatIso.mapHomologicalComplex α c).inv.app C).f x✝ = α.inv.app (C.X x✝) - CategoryTheory.Functor.mapHomologicalComplexIdIso_hom_app_f 📋 Mathlib.Algebra.Homology.Additive
{ι : Type u_1} (W₁ : Type u_3) [CategoryTheory.Category.{v_2, u_3} W₁] [CategoryTheory.Limits.HasZeroMorphisms W₁] (c : ComplexShape ι) (X : HomologicalComplex W₁ c) (i : ι) : ((CategoryTheory.Functor.mapHomologicalComplexIdIso W₁ c).hom.app X).f i = CategoryTheory.CategoryStruct.id (X.X i) - CategoryTheory.Functor.mapHomologicalComplexIdIso_inv_app_f 📋 Mathlib.Algebra.Homology.Additive
{ι : Type u_1} (W₁ : Type u_3) [CategoryTheory.Category.{v_2, u_3} W₁] [CategoryTheory.Limits.HasZeroMorphisms W₁] (c : ComplexShape ι) (X : HomologicalComplex W₁ c) (i : ι) : ((CategoryTheory.Functor.mapHomologicalComplexIdIso W₁ c).inv.app X).f i = CategoryTheory.CategoryStruct.id (X.X i) - HomologicalComplex.neg_f_apply 📋 Mathlib.Algebra.Homology.Additive
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} (f : C ⟶ D) (i : ι) : (-f).f i = -f.f i - CategoryTheory.Functor.mapHomologicalComplex_map_f 📋 Mathlib.Algebra.Homology.Additive
{ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [CategoryTheory.Category.{v_2, u_3} W₁] [CategoryTheory.Category.{v_3, u_4} W₂] [CategoryTheory.Limits.HasZeroMorphisms W₁] [CategoryTheory.Limits.HasZeroMorphisms W₂] (F : CategoryTheory.Functor W₁ W₂) [F.PreservesZeroMorphisms] (c : ComplexShape ι) {X✝ Y✝ : HomologicalComplex W₁ c} (f : X✝ ⟶ Y✝) (i : ι) : ((F.mapHomologicalComplex c).map f).f i = F.map (f.f i) - CategoryTheory.NatTrans.mapHomologicalComplex_comp 📋 Mathlib.Algebra.Homology.Additive
{ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [CategoryTheory.Category.{v_2, u_3} W₁] [CategoryTheory.Category.{v_3, u_4} W₂] [CategoryTheory.Limits.HasZeroMorphisms W₁] [CategoryTheory.Limits.HasZeroMorphisms W₂] (c : ComplexShape ι) {F G H : CategoryTheory.Functor W₁ W₂} [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] [H.PreservesZeroMorphisms] (α : F ⟶ G) (β : G ⟶ H) : CategoryTheory.NatTrans.mapHomologicalComplex (CategoryTheory.CategoryStruct.comp α β) c = CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.mapHomologicalComplex α c) (CategoryTheory.NatTrans.mapHomologicalComplex β c) - CategoryTheory.Equivalence.mapHomologicalComplex_counitIso 📋 Mathlib.Algebra.Homology.Additive
{ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [CategoryTheory.Category.{v_2, u_3} W₁] [CategoryTheory.Category.{v_3, u_4} W₂] [CategoryTheory.Limits.HasZeroMorphisms W₁] [CategoryTheory.Limits.HasZeroMorphisms W₂] (e : W₁ ≌ W₂) [e.functor.PreservesZeroMorphisms] (c : ComplexShape ι) : (e.mapHomologicalComplex c).counitIso = CategoryTheory.NatIso.mapHomologicalComplex e.counitIso c ≪≫ CategoryTheory.Functor.mapHomologicalComplexIdIso W₂ c - CategoryTheory.Functor.mapHomologicalComplexCompIso_hom_app_f 📋 Mathlib.Algebra.Homology.Additive
{ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} {W₃ : Type u_5} [CategoryTheory.Category.{v_2, u_3} W₁] [CategoryTheory.Category.{v_3, u_4} W₂] [CategoryTheory.Category.{v_4, u_5} W₃] [CategoryTheory.Limits.HasZeroMorphisms W₁] [CategoryTheory.Limits.HasZeroMorphisms W₂] [CategoryTheory.Limits.HasZeroMorphisms W₃] {F : CategoryTheory.Functor W₁ W₂} {G : CategoryTheory.Functor W₂ W₃} {H : CategoryTheory.Functor W₁ W₃} (e : F.comp G ≅ H) [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] [H.PreservesZeroMorphisms] (c : ComplexShape ι) (C : HomologicalComplex W₁ c) (x✝ : ι) : ((CategoryTheory.Functor.mapHomologicalComplexCompIso e c).hom.app C).f x✝ = e.hom.app (C.X x✝) - CategoryTheory.Functor.mapHomologicalComplexCompIso_inv_app_f 📋 Mathlib.Algebra.Homology.Additive
{ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} {W₃ : Type u_5} [CategoryTheory.Category.{v_2, u_3} W₁] [CategoryTheory.Category.{v_3, u_4} W₂] [CategoryTheory.Category.{v_4, u_5} W₃] [CategoryTheory.Limits.HasZeroMorphisms W₁] [CategoryTheory.Limits.HasZeroMorphisms W₂] [CategoryTheory.Limits.HasZeroMorphisms W₃] {F : CategoryTheory.Functor W₁ W₂} {G : CategoryTheory.Functor W₂ W₃} {H : CategoryTheory.Functor W₁ W₃} (e : F.comp G ≅ H) [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] [H.PreservesZeroMorphisms] (c : ComplexShape ι) (C : HomologicalComplex W₁ c) (x✝ : ι) : ((CategoryTheory.Functor.mapHomologicalComplexCompIso e c).inv.app C).f x✝ = e.inv.app (C.X x✝) - HomologicalComplex.Hom.fAddMonoidHom 📋 Mathlib.Algebra.Homology.Additive
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} (i : ι) : (C₁ ⟶ C₂) →+ (C₁.X i ⟶ C₂.X i) - HomologicalComplex.zsmul_f_apply 📋 Mathlib.Algebra.Homology.Additive
{ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} (n : ℤ) (f : C ⟶ D) (i : ι) : (n • f).f i = n • f.f i - CategoryTheory.Equivalence.mapHomologicalComplex_unitIso 📋 Mathlib.Algebra.Homology.Additive
{ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [CategoryTheory.Category.{v_2, u_3} W₁] [CategoryTheory.Category.{v_3, u_4} W₂] [CategoryTheory.Limits.HasZeroMorphisms W₁] [CategoryTheory.Limits.HasZeroMorphisms W₂] (e : W₁ ≌ W₂) [e.functor.PreservesZeroMorphisms] (c : ComplexShape ι) : (e.mapHomologicalComplex c).unitIso = (CategoryTheory.Functor.mapHomologicalComplexIdIso W₁ c).symm ≪≫ CategoryTheory.NatIso.mapHomologicalComplex e.unitIso c - ChainComplex.map_chain_complex_of 📋 Mathlib.Algebra.Homology.Additive
{W₁ : Type u_3} {W₂ : Type u_4} [CategoryTheory.Category.{v_2, u_3} W₁] [CategoryTheory.Category.{v_3, u_4} W₂] [CategoryTheory.Limits.HasZeroMorphisms W₁] [CategoryTheory.Limits.HasZeroMorphisms W₂] {α : Type u_6} [AddRightCancelSemigroup α] [One α] [DecidableEq α] (F : CategoryTheory.Functor W₁ W₂) [F.PreservesZeroMorphisms] (X : α → W₁) (d : (n : α) → X (n + 1) ⟶ X n) (sq : ∀ (n : α), CategoryTheory.CategoryStruct.comp (d (n + 1)) (d n) = 0) : (F.mapHomologicalComplex (ComplexShape.down α)).obj (ChainComplex.of X d sq) = ChainComplex.of (fun n => F.obj (X n)) (fun n => F.map (d n)) ⋯
About
Loogle searches Lean and Mathlib definitions and theorems.
You can use Loogle from within the Lean4 VSCode language extension
using the Loogle command from the command palette. You can also try the
#loogle command from LeanSearchClient,
the CLI version, the Loogle
VS Code extension, the lean.nvim
integration or the Zulip bot.
Usage
Loogle finds definitions and lemmas in various ways:
By constant:
🔍Real.sin
finds all lemmas whose statement somehow mentions the sine function.By lemma name substring:
🔍"differ"
finds all lemmas that have"differ"somewhere in their lemma name.By subexpression:
🔍_ * (_ ^ _)
finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.The pattern can also be non-linear, as in
🔍Real.sqrt ?a * Real.sqrt ?aIf the pattern has parameters, they are matched in any order. Both of these will find
List.map:
🔍(?a -> ?b) -> List ?a -> List ?b
🔍List ?a -> (?a -> ?b) -> List ?bBy main conclusion:
🔍|- tsum _ = _ * tsum _
finds all lemmas where the conclusion (the subexpression to the right of all→and∀) has the given shape.As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
🔍|- _ < _ → tsum _ < tsum _
will findtsum_lt_tsumeven though the hypothesisf i < g iis not the last.You can filter for definitions vs theorems: Using
⊢ (_ : Type _)finds all definitions which provide data while⊢ (_ : Prop)finds all theorems (and definitions of proofs).
If you pass more than one such search filter, separated by commas
Loogle will return lemmas which match all of them. The
search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin
and tsum, have "two" as a substring of the
lemma name, include a product and a power somewhere in the type,
and have a hypothesis of the form _ < _ (if
there were any such lemmas). Metavariables (?a) are
assigned independently in each filter.
The #lucky button will directly send you to the
documentation of the first hit.
Source code
You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.
This is Loogle revision 9f11169 serving mathlib revision ce5dd8c