Structures · Algebra
HomologicalComplex.HasHomotopyCofiber
A morphism of homological complexes φ : F ⟶ G has a homotopy cofiber if for all
indices i and j such that c.Rel i j, the binary biproduct F.X j ⊞ G.X i exists.
- Defined in
- Mathlib.Algebra.Homology.HomotopyCofiber
- Shape
- One type argument · adds hasBinaryBiproduct
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by260
- CochainComplex.mappingCone
- CochainComplex.mappingCone.inr
- CochainComplex.mappingCone.inl
- HomologicalComplex.homotopyCofiber.X
- CochainComplex.mappingCone.fst
- CochainComplex.mappingCone.snd
- CochainComplex.mappingCocone
- HomologicalComplex.homotopyCofiber.inrX
- HomologicalComplex.homotopyCofiber
- HomologicalComplex.homotopyCofiber.inlX
- HomologicalComplex.homotopyCofiber.sndX
- HomologicalComplex.homotopyCofiber.fstX
- HomologicalComplex.homotopyCofiber.XIsoBiprod
- CochainComplex.mappingCone.descCochain
- CochainComplex.mappingCone.desc
- CochainComplex.mappingCone.liftCochain
- HomologicalComplex.homotopyCofiber.inr
- HomologicalComplex.homotopyCofiber.d
- HomologicalComplex.homotopyCofiber.desc
- CochainComplex.mappingCocone.fst
- HomologicalComplex.homotopyCofiber.XIso
- CochainComplex.mappingCocone.liftCochain
- CochainComplex.mappingCone.lift
- HomologicalComplex.HasHomotopyCofiber.hasBinaryBiproduct
- CochainComplex.mappingCocone.descCochain
- CochainComplex.mappingCocone.inr
- CochainComplex.mappingCocone.inl
- CochainComplex.mappingCocone.snd
- HomologicalComplex.homotopyCofiber.inrCompHomotopy
- CochainComplex.mappingCone.inr_f_fst_v
- CochainComplex.mappingCone.ext_from_iff
- CochainComplex.mappingCocone.lift
- HomologicalComplex.homotopyCofiber.inrX_sndX
- CochainComplex.mappingCone.inr_f_desc_f
- CochainComplex.mappingCone.descCocycle
- CochainComplex.mappingCone.inr_f_snd_v
- CochainComplex.mappingCone.inl_v_fst_v
- HomologicalComplex.homotopyCofiber.inrX_fstX
- HomologicalComplex.homotopyCofiber.mapHomologicalComplexObjXIso
- HomologicalComplex.homotopyCofiber.inlX_sndX
- CochainComplex.mappingCone.inl_v_snd_v
- HomologicalComplex.homotopyCofiber.mapArrowHom
- HomologicalComplex.homotopyCofiber.inlX_fstX_assoc
- HomologicalComplex.homotopyCofiber.inlX_sndX_assoc
- CochainComplex.mappingCone.liftCocycle
- CochainComplex.mappingCone.descCocycle_coe
- HomologicalComplex.homotopyCofiber.inlX_fstX
- CochainComplex.mappingCone.inl_v_fst_v_assoc
- CochainComplex.mappingCocone.desc
- CochainComplex.mappingCocone.liftCocycle
Ancestors0
No ancestors.