Lifting

📁 Source: Mathlib/Algebra/Homology/ModelCategory/Lifting.lean

Statistics

Metric	Count
Definitions cochain₀, cochain₁, cocycle₁, cocycle₁'	4
Theorems coe_cocycle₁'_v_comp_eq_zero, coe_cocycle₁'_v_comp_eq_zero_assoc, comp_coe_cocycle₁_comp, comp_coe_cocyle₁'_v_eq_zero, comp_coe_cocyle₁'_v_eq_zero_assoc, exists_hom, hasLift, π_f_cochain₁_v_ι_f, π_f_cochain₁_v_ι_f_assoc	9
Total	13

CochainComplex.Lifting

Definitions

Name	Category	Theorems
cochain₀ 📖	CompOp	—
cochain₁ 📖	CompOp	2 math math: π_f_cochain₁_v_ι_f, π_f_cochain₁_v_ι_f_assoc
cocycle₁ 📖	CompOp	1 math math: comp_coe_cocycle₁_comp
cocycle₁' 📖	CompOp	8 math math: π_f_cochain₁_v_ι_f, comp_coe_cocyle₁'_v_eq_zero, exists_hom, π_f_cochain₁_v_ι_f_assoc, coe_cocycle₁'_v_comp_eq_zero, comp_coe_cocyle₁'_v_eq_zero_assoc, comp_coe_cocycle₁_comp, coe_cocycle₁'_v_comp_eq_zero_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_cocycle₁'_v_comp_eq_zero 📖	mathematical	CategoryTheory.CommSq CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CochainComplex.HomComplex.Cochain.v CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle cocycle₁' HomologicalComplex.Hom.f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.CommSq.map CategoryTheory.CommSq.LiftStruct.fac_right add_zero CochainComplex.HomComplex.δ_zero_cochain_v CochainComplex.HomComplex.Cochain.ofHoms_v CategoryTheory.Preadditive.sub_comp CategoryTheory.Category.assoc HomologicalComplex.Hom.comm Mathlib.Tactic.Reassoc.eq_whisker' sub_self
coe_cocycle₁'_v_comp_eq_zero_assoc 📖	mathematical	CategoryTheory.CommSq CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CochainComplex.HomComplex.Cochain.v CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle cocycle₁' HomologicalComplex.Hom.f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.CommSq.map CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' coe_cocycle₁'_v_comp_eq_zero
comp_coe_cocycle₁_comp 📖	mathematical	CategoryTheory.CommSq CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver HomologicalComplex.instZeroHom_1	CochainComplex.HomComplex.Cochain.comp CategoryTheory.Abelian.toPreadditive CochainComplex.HomComplex.Cochain.ofHom CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle cocycle₁ add_zero AddMonoid.toAddZeroClass Int.instAddMonoid zero_add cocycle₁'	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.CommSq.map CochainComplex.HomComplex.Cochain.ext add_zero zero_add CochainComplex.HomComplex.Cochain.zero_cochain_comp_v CochainComplex.HomComplex.Cochain.ofHom_v CochainComplex.HomComplex.Cochain.comp_zero_cochain_v π_f_cochain₁_v_ι_f
comp_coe_cocyle₁'_v_eq_zero 📖	mathematical	CategoryTheory.CommSq CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.Hom.f CochainComplex.HomComplex.Cochain.v CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle cocycle₁' Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.CommSq.map CategoryTheory.CommSq.LiftStruct.fac_left add_zero CochainComplex.HomComplex.δ_zero_cochain_v CochainComplex.HomComplex.Cochain.ofHoms_v CategoryTheory.Preadditive.comp_sub CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' HomologicalComplex.Hom.comm HomologicalComplex.Hom.comm_assoc sub_self
comp_coe_cocyle₁'_v_eq_zero_assoc 📖	mathematical	CategoryTheory.CommSq CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.Hom.f CochainComplex.HomComplex.Cochain.v CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle cocycle₁' Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.CommSq.map CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_coe_cocyle₁'_v_eq_zero
exists_hom 📖	mathematical	CategoryTheory.CommSq CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver HomologicalComplex.instZeroHom_1	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.CategoryStruct.comp HomologicalComplex.Hom.f CochainComplex.HomComplex.Cochain.v CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle cocycle₁'	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.CommSq.map CategoryTheory.Limits.Cofork.IsColimit.epi HomologicalComplex.instPreservesZeroMorphismsEval HomologicalComplex.instPreservesColimitEval CategoryTheory.Limits.instHasColimitCompOfPreservesColimit CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Limits.hasCokernels_of_hasCoequalizers HomologicalComplex.instHasColimitsOfShape CategoryTheory.Abelian.hasCoequalizers CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit HomologicalComplex.instPreservesColimitsOfShapeEvalOfHasColimitsOfShape comp_coe_cocyle₁'_v_eq_zero HomologicalComplex.instPreservesLimitEval CategoryTheory.Limits.instHasLimitCompOfPreservesLimit CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Limits.hasKernels_of_hasEqualizers HomologicalComplex.instHasLimitsOfShape CategoryTheory.Abelian.hasEqualizers CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit HomologicalComplex.instPreservesLimitsOfShapeEvalOfHasLimitsOfShape CategoryTheory.cancel_epi HomologicalComplex.instEpiFOfHasFiniteColimits CategoryTheory.Abelian.hasFiniteColimits CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' coe_cocycle₁'_v_comp_eq_zero CategoryTheory.Limits.comp_zero
hasLift 📖	mathematical	CategoryTheory.CommSq CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver HomologicalComplex.instZeroHom_1 CochainComplex.HomComplex.δ CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle cocycle₁	CategoryTheory.CommSq.HasLift CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.CommSq.map add_zero zero_add comp_coe_cocycle₁_comp CochainComplex.HomComplex.Cochain.ext CochainComplex.HomComplex.Cochain.congr_v CochainComplex.HomComplex.Cochain.v.congr_simp CochainComplex.HomComplex.δ_sub CochainComplex.HomComplex.δ_ofHom_comp CochainComplex.HomComplex.δ_comp_ofHom CochainComplex.HomComplex.δ_zero_cochain_v CochainComplex.HomComplex.Cochain.ofHoms_v CochainComplex.HomComplex.Cochain.zero_cochain_comp_v CochainComplex.HomComplex.Cochain.ofHom_v CochainComplex.HomComplex.Cochain.comp_zero_cochain_v CategoryTheory.Preadditive.sub_comp CategoryTheory.Category.assoc CategoryTheory.Preadditive.comp_sub HomologicalComplex.Hom.comm_assoc sub_self HomologicalComplex.hom_ext CategoryTheory.CommSq.LiftStruct.fac_left Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.Limits.zero_comp sub_zero CategoryTheory.Limits.comp_zero CategoryTheory.CommSq.LiftStruct.fac_right
π_f_cochain₁_v_ι_f 📖	mathematical	CategoryTheory.CommSq CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver HomologicalComplex.instZeroHom_1	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.Hom.f CochainComplex.HomComplex.Cochain.v cochain₁ CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle cocycle₁'	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.CommSq.map exists_hom
π_f_cochain₁_v_ι_f_assoc 📖	mathematical	CategoryTheory.CommSq CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver HomologicalComplex.instZeroHom_1	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.Hom.f CochainComplex.HomComplex.Cochain.v cochain₁ CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle cocycle₁'	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.CommSq.map CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' π_f_cochain₁_v_ι_f

---

← Back to Index