Structures · Algebra
ComplexShape.Embedding.IsTruncGE
The condition that the image of the map e.f of an embedding of
complex shapes e : Embedding c c' is stable by c'.next.
- Defined in
- Mathlib.Algebra.Homology.Embedding.Basic
- Shape
- One type argument · adds mem_next
Extends1
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- Nat
How is a type an instance?
Loading the hierarchy index…
Assumed by89
- HomologicalComplex.truncGE'
- HomologicalComplex.truncGE
- HomologicalComplex.truncGE'XIso
- HomologicalComplex.truncGE'XIsoOpcycles
- HomologicalComplex.πTruncGE
- HomologicalComplex.restrictionToTruncGE'
- HomologicalComplex.truncGE'Map
- HomologicalComplex.truncGEMap
- HomologicalComplex.isIso_restrictionToTruncGE'
- ComplexShape.Embedding.truncGEFunctor
- ComplexShape.Embedding.truncGE'Functor
- HomologicalComplex.truncGE'Map_f_eq
- HomologicalComplex.πTruncGE_naturality
- HomologicalComplex.truncGE'Map_f_eq_opcyclesMap
- HomologicalComplex.restrictionToTruncGE'.f
- HomologicalComplex.truncGE.rightHomologyMapData
- HomologicalComplex.truncGE'Map_comp
- HomologicalComplex.truncGE'_d_eq_fromOpcycles
- HomologicalComplex.shortComplexTruncLEX₃ToTruncGE
- ComplexShape.Embedding.next_f
- HomologicalComplex.restrictionToTruncGE'_naturality
- HomologicalComplex.truncGE'.homologyData
- HomologicalComplex.restrictionToTruncGE'.f_eq_iso_hom_pOpcycles_iso_inv
- HomologicalComplex.truncGE'.d
- HomologicalComplex.acyclic_truncGE_iff_isSupportedOutside
- HomologicalComplex.quasiIsoAt_πTruncGE
- HomologicalComplex.restrictionToTruncGE'.f_eq_iso_hom_iso_inv
- HomologicalComplex.g_shortComplexTruncLEX₃ToTruncGE
- HomologicalComplex.quasiIso_truncGEMap_iff
- HomologicalComplex.truncGE'_d_eq
- ComplexShape.Embedding.mem_next
- HomologicalComplex.restrictionToTruncGE'_hasLift
- HomologicalComplex.restrictionToTruncGE'_f_eq_iso_hom_iso_inv
- HomologicalComplex.quasiIso_πTruncGE_iff_isSupported
- HomologicalComplex.truncGEMap_comp
- HomologicalComplex.truncGE'Map_id
- ComplexShape.Embedding.IsTruncGE.mem_next
- ComplexShape.Embedding.πTruncGENatTrans
- HomologicalComplex.truncGEMap_id
- ComplexShape.Embedding.restrictionToTruncGE'NatTrans
- HomologicalComplex.truncGE'.quasiIsoAt_restrictionToTruncGE'
- HomologicalComplex.isIso_πTruncGE_iff
- HomologicalComplex.restrictionToTruncGE'_f_eq_iso_hom_pOpcycles_iso_inv
- HomologicalComplex.truncGE'.d_comp_d
- HomologicalComplex.restrictionToTruncGE'.comm
- HomologicalComplex.truncGE'.hasHomology_sc'_of_not_mem_boundary
- HomologicalComplex.truncGE'.isLimitKernelFork
- HomologicalComplex.truncGE'.homologyι_truncGE'XIsoOpcycles_inv_d
- HomologicalComplex.restrictionToTruncGE'.comm_assoc
- HomologicalComplex.truncGE'.truncGE'_hasHomology