QuasiIso

📁 Source: Mathlib/Algebra/Homology/ShortComplex/QuasiIso.lean

Statistics

Metric	Count
Definitions QuasiIso, QuasiIso	2
Theorems quasiIso_iff, isIso, isIso', quasiIso_iff, quasiIso_comp, quasiIso_iff, quasiIso_iff_comp_left, quasiIso_iff_comp_right, quasiIso_iff_isIso_descOpcycles, quasiIso_iff_isIso_homologyMap', quasiIso_iff_isIso_leftHomologyMap', quasiIso_iff_isIso_liftCycles, quasiIso_iff_isIso_rightHomologyMap', quasiIso_iff_of_arrow_mk_iso, quasiIso_of_arrow_mk_iso, quasiIso_of_comp_left, quasiIso_of_comp_right, quasiIso_of_epi_of_isIso_of_mono, quasiIso_of_isIso, quasiIso_opMap, quasiIso_opMap_iff, quasiIso_unopMap	22
Total	24

CategoryTheory.ShortComplex

Definitions

Name	Category	Theorems
QuasiIso 📖	CompData	35 math math: quasiIso_of_epi_of_isIso_of_mono, quasiIso_iff_isIso_rightHomologyMap', quasiIso_of_retract, RightHomologyMapData.quasiIso_map_iff, quasiIso_iff_isIso_homologyMap', quasiIso_iff_isIso_descOpcycles, ChainComplex.quasiIsoAt₀_iff, quasiIso_iff_comp_right, quasiIso_map_of_preservesLeftHomology, LeftHomologyMapData.quasiIso_map_iff, quasiIso_iff_comp_left, quasiIso_map_iff_of_preservesRightHomology, quasiIso_iff_of_zeros', quasiIso_iff_of_zeros, quasiIso_map_iff_of_preservesLeftHomology, QuasiIsoAt.quasiIso, quasiIso_opMap, quasiIsoAt_iff', CochainComplex.quasiIsoAt₀_iff, quasiIso_iff, quasiIso_iff_evaluation, LeftHomologyMapData.quasiIso_iff, quasiIso_of_comp_right, quasiIso_comp, quasiIso_iff_isIso_leftHomologyMap', quasiIso_iff_of_arrow_mk_iso, quasiIsoAt_iff, quasiIso_of_comp_left, quasiIso_unopMap, quasiIso_of_arrow_mk_iso, quasiIso_map_of_preservesRightHomology, quasiIso_of_isIso, quasiIso_opMap_iff, RightHomologyMapData.quasiIso_iff, quasiIso_iff_isIso_liftCycles

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
quasiIso_comp 📖	mathematical	—	QuasiIso CategoryTheory.CategoryStruct.comp CategoryTheory.ShortComplex CategoryTheory.Category.toCategoryStruct instCategory	—	quasiIso_iff homologyMap_comp CategoryTheory.IsIso.comp_isIso
quasiIso_iff 📖	mathematical	—	QuasiIso CategoryTheory.IsIso homology homologyMap	—	QuasiIso.isIso
quasiIso_iff_comp_left 📖	mathematical	—	QuasiIso CategoryTheory.CategoryStruct.comp CategoryTheory.ShortComplex CategoryTheory.Category.toCategoryStruct instCategory	—	quasiIso_of_comp_left quasiIso_comp
quasiIso_iff_comp_right 📖	mathematical	—	QuasiIso CategoryTheory.CategoryStruct.comp CategoryTheory.ShortComplex CategoryTheory.Category.toCategoryStruct instCategory	—	quasiIso_of_comp_right quasiIso_comp
quasiIso_iff_isIso_descOpcycles 📖	mathematical	g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X₂ X₃ CategoryTheory.Limits.HasZeroMorphisms.zero f X₁	QuasiIso CategoryTheory.IsIso opcycles hasRightHomology_of_hasHomology descOpcycles Hom.τ₂	—	hasRightHomology_of_hasHomology f_pOpcycles Hom.comm₁₂ CategoryTheory.Limits.comp_zero p_descOpcycles CategoryTheory.Category.comp_id RightHomologyData.ofZeros_g' RightHomologyData.ofIsColimitCokernelCofork_g' CategoryTheory.Limits.zero_comp CategoryTheory.Category.id_comp RightHomologyMapData.quasiIso_iff
quasiIso_iff_isIso_homologyMap' 📖	mathematical	—	QuasiIso CategoryTheory.IsIso LeftHomologyData.H HomologyData.left homologyMap'	—	quasiIso_iff_isIso_leftHomologyMap'
quasiIso_iff_isIso_leftHomologyMap' 📖	mathematical	—	QuasiIso CategoryTheory.IsIso LeftHomologyData.H leftHomologyMap'	—	LeftHomologyMapData.quasiIso_iff LeftHomologyMapData.leftHomologyMap'_eq
quasiIso_iff_isIso_liftCycles 📖	mathematical	f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X₁ X₂ CategoryTheory.Limits.HasZeroMorphisms.zero g X₃	QuasiIso CategoryTheory.IsIso cycles hasLeftHomology_of_hasHomology liftCycles Hom.τ₂	—	hasLeftHomology_of_hasHomology iCycles_g Hom.comm₂₃ CategoryTheory.Limits.zero_comp liftCycles_i CategoryTheory.Category.id_comp LeftHomologyData.ofZeros_f' LeftHomologyData.ofIsLimitKernelFork_f' CategoryTheory.Limits.comp_zero CategoryTheory.Category.comp_id LeftHomologyMapData.quasiIso_iff
quasiIso_iff_isIso_rightHomologyMap' 📖	mathematical	—	QuasiIso CategoryTheory.IsIso RightHomologyData.H rightHomologyMap'	—	RightHomologyMapData.quasiIso_iff RightHomologyMapData.rightHomologyMap'_eq
quasiIso_iff_of_arrow_mk_iso 📖	mathematical	—	QuasiIso	—	quasiIso_of_arrow_mk_iso
quasiIso_of_arrow_mk_iso 📖	mathematical	—	QuasiIso	—	CategoryTheory.Arrow.w_mk_right_assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id quasiIso_comp quasiIso_of_isIso CategoryTheory.Arrow.isIso_left CategoryTheory.Iso.isIso_inv CategoryTheory.Arrow.isIso_right CategoryTheory.Iso.isIso_hom
quasiIso_of_comp_left 📖	mathematical	—	QuasiIso	—	quasiIso_iff CategoryTheory.IsIso.of_isIso_comp_left homologyMap_comp
quasiIso_of_comp_right 📖	mathematical	—	QuasiIso	—	quasiIso_iff CategoryTheory.IsIso.of_isIso_comp_right homologyMap_comp
quasiIso_of_epi_of_isIso_of_mono 📖	mathematical	—	QuasiIso	—	hasLeftHomology_of_hasHomology LeftHomologyMapData.quasiIso_iff CategoryTheory.IsIso.id
quasiIso_of_isIso 📖	mathematical	—	QuasiIso	—	CategoryTheory.Iso.isIso_hom
quasiIso_opMap 📖	mathematical	—	QuasiIso Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite op instHasHomologyOppositeOp opMap	—	instHasHomologyOppositeOp quasiIso_opMap_iff
quasiIso_opMap_iff 📖	mathematical	—	QuasiIso Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite op instHasHomologyOppositeOp opMap	—	instHasHomologyOppositeOp LeftHomologyMapData.quasiIso_iff RightHomologyMapData.quasiIso_iff CategoryTheory.isIso_of_op CategoryTheory.isIso_op
quasiIso_unopMap 📖	mathematical	—	QuasiIso unop unopMap	—	instHasHomologyOppositeOp quasiIso_opMap_iff

CategoryTheory.ShortComplex.LeftHomologyMapData

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
quasiIso_iff 📖	mathematical	—	CategoryTheory.ShortComplex.QuasiIso CategoryTheory.IsIso CategoryTheory.ShortComplex.LeftHomologyData.H φH	—	CategoryTheory.ShortComplex.quasiIso_iff homologyMap_eq CategoryTheory.IsIso.of_isIso_comp_right CategoryTheory.Iso.isIso_inv CategoryTheory.IsIso.of_isIso_comp_left CategoryTheory.Iso.isIso_hom CategoryTheory.IsIso.comp_isIso

CategoryTheory.ShortComplex.QuasiIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isIso 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.ShortComplex.homology CategoryTheory.ShortComplex.homologyMap	—	isIso'
isIso' 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.ShortComplex.homology CategoryTheory.ShortComplex.homologyMap	—	—

CategoryTheory.ShortComplex.RightHomologyMapData

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
quasiIso_iff 📖	mathematical	—	CategoryTheory.ShortComplex.QuasiIso CategoryTheory.IsIso CategoryTheory.ShortComplex.RightHomologyData.H φH	—	CategoryTheory.ShortComplex.quasiIso_iff homologyMap_eq CategoryTheory.IsIso.of_isIso_comp_right CategoryTheory.Iso.isIso_inv CategoryTheory.IsIso.of_isIso_comp_left CategoryTheory.Iso.isIso_hom CategoryTheory.IsIso.comp_isIso

(root)

Definitions

Name	Category	Theorems
QuasiIso 📖	CompData	46 math math: HomologicalComplex.quasiIso_extendMap_iff, CategoryTheory.ProjectiveResolution.quasiIso, CochainComplex.quasiIso_truncLEMap_iff, quasiIso_of_comp_left, HomologicalComplex.quasiIso_map_of_preservesHomology, quasiIso_of_isIso, HomologicalComplex.mem_quasiIso_iff, HomologicalComplex.quasiIso_map_iff_of_preservesHomology, HomologicalComplex.quasiIso_πTruncGE_iff_isSupported, HomologicalComplex.quasiIso_iff_evaluation, quasiIso_iff_of_arrow_mk_iso, HomotopyEquiv.quasiIso_hom, HomologicalComplex.instQuasiIsoMapOppositeSymmUnopFunctorOp, HomotopyEquiv.quasiIso_inv, HomologicalComplex.HomologySequence.quasiIso_τ₃, CochainComplex.quasiIso_truncGEMap_iff, CochainComplex.quasiIso_shift_iff, quasiIso_iff_comp_left, quasiIso_of_arrow_mk_iso, CochainComplex.instQuasiIsoIntιTruncLEOfIsLE, HomologicalComplex.instQuasiIsoExtendMap, quasiIso_comp, CochainComplex.cm5b.instQuasiIsoIntP, CochainComplex.mappingCone.quasiIso_descShortComplex, quasiIso_of_comp_right, CochainComplex.quasiIso_πTruncGE_iff, quasiIso_iff, Rep.standardComplex.quasiIso_forget₂_εToSingle₀, CochainComplex.instQuasiIsoIntMapHomologicalComplexUpShiftFunctor, HomologicalComplex.quasiIso_ιTruncLE_iff_isSupported, CochainComplex.quasiIso_ιTruncLE_iff, HomologicalComplex.instQuasiIsoOppositeMapSymmOpFunctorOp, Rep.standardComplex.instQuasiIsoNatεToSingle₀, CategoryTheory.InjectiveResolution.instQuasiIsoIntι', Rep.FiniteCyclicGroup.resolution_quasiIso, HomologicalComplex.quasiIso_opFunctor_map_iff, CategoryTheory.ProjectiveResolution.instQuasiIsoIntπ', HomologicalComplex.quasiIso_truncGEMap_iff, HomologicalComplex.quasiIso_unopFunctor_map_iff, quasiIso_iff_comp_right, quasiIso_of_retractArrow, HomologicalComplex.instQuasiIsoShortComplexTruncLEX₃ToTruncGE, DerivedCategory.isIso_Q_map_iff_quasiIso, CategoryTheory.InjectiveResolution.quasiIso, CochainComplex.instQuasiIsoIntπTruncGEOfIsGE, HomologicalComplex.quasiIso_truncLEMap_iff

---

← Back to Index