QuasiIso

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

Statistics

Metric	Count
Definitions quasiIso, QuasiIsoAt, isoOfQuasiIsoAt	3
Theorems quasiIsoAt₀_iff, quasiIsoAt₀_iff, instHasTwoOutOfThreePropertyQuasiIso, instIsMultiplicativeQuasiIso, instIsStableUnderRetractsQuasiIso, instRespectsIsoQuasiIso, mem_quasiIso_iff, quasiIsoAt_map_iff_of_preservesHomology, quasiIsoAt_map_of_preservesHomology, quasiIso_map_iff_of_preservesHomology, quasiIso_map_of_preservesHomology, quasiIsoAt_hom, quasiIsoAt_inv, quasiIso_hom, quasiIso_inv, quasiIsoAt, quasiIso, exactAt_iff_of_quasiIsoAt, homotopyEquivalences_le_quasiIso, instIsIsoHomologyMapOfQuasiIsoAt, isoOfQuasiIsoAt_hom, isoOfQuasiIsoAt_hom_inv_id, isoOfQuasiIsoAt_hom_inv_id_assoc, isoOfQuasiIsoAt_inv_hom_id, isoOfQuasiIsoAt_inv_hom_id_assoc, quasiIsoAt_comp, quasiIsoAt_iff, quasiIsoAt_iff', quasiIsoAt_iff_comp_left, quasiIsoAt_iff_comp_right, quasiIsoAt_iff_exactAt, quasiIsoAt_iff_exactAt', quasiIsoAt_iff_isIso_homologyMap, quasiIsoAt_of_comp_left, quasiIsoAt_of_comp_right, quasiIsoAt_of_isIso, quasiIsoAt_of_retract, quasiIso_comp, quasiIso_iff, quasiIso_iff_comp_left, quasiIso_iff_comp_right, quasiIso_iff_of_arrow_mk_iso, quasiIso_of_arrow_mk_iso, quasiIso_of_comp_left, quasiIso_of_comp_right, quasiIso_of_isIso, quasiIso_of_retractArrow	47
Total	50

ChainComplex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
quasiIsoAt₀_iff 📖	mathematical	—	QuasiIsoAt ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne CategoryTheory.ShortComplex.QuasiIso CategoryTheory.Functor.obj HomologicalComplex HomologicalComplex.instCategory CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory HomologicalComplex.shortComplexFunctor' CategoryTheory.Functor.map	—	AddRightCancelSemigroup.toIsRightCancelAdd quasiIsoAt_iff' prev zero_add next_nat_zero

CochainComplex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
quasiIsoAt₀_iff 📖	mathematical	—	QuasiIsoAt ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne CategoryTheory.ShortComplex.QuasiIso CategoryTheory.Functor.obj HomologicalComplex HomologicalComplex.instCategory CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory HomologicalComplex.shortComplexFunctor' CategoryTheory.Functor.map	—	AddRightCancelSemigroup.toIsRightCancelAdd quasiIsoAt_iff' prev_nat_zero next zero_add

HomologicalComplex

Definitions

Name	Category	Theorems
quasiIso 📖	CompOp	26 math math: DerivedCategory.instIsLocalizationCochainComplexIntQQuasiIsoUp, CategoryTheory.ShortComplex.ShortExact.instHasSmallLocalizedShiftedHomHomologicalComplexIntUpQuasiIsoX₃CochainComplexMapSingleFunctorOfNatX₁, homotopyEquivalences_le_quasiIso, CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoFactorsh_hom_app_assoc, instIsStableUnderRetractsQuasiIso, HomologicalComplexUpToQuasiIso.instIsLocalizationHomologicalComplexCompHomotopyCategoryQuotientQhQuasiIso, CochainComplex.instIsCompatibleWithShiftHomologicalComplexIntUpQuasiIso, mem_quasiIso_iff, HomologicalComplexUpToQuasiIso.Q_inverts_homotopyEquivalences, instRespectsIsoQuasiIso, CategoryTheory.Functor.mapHomologicalComplex_upToQuasiIso_Q_inverts_quasiIso, HomotopyCategory.quasiIso_eq_quasiIso_map_quotient, instIsMultiplicativeQuasiIso, HomologicalComplexUpToQuasiIso.Q_map_eq_of_homotopy, CategoryTheory.HasExt.hasSmallLocalizedShiftedHom_of_isLE_of_isGE, CategoryTheory.HasExt.instHasSmallLocalizedShiftedHomHomologicalComplexIntUpQuasiIsoOfIsGEOfIsLEOfNat, CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoLocalizerMorphism_functor, CategoryTheory.instHasSmallLocalizedShiftedHomHomologicalComplexIntUpQuasiIsoObjCochainComplexCompSingleFunctorOfNatOfHasExt, HomologicalComplexUpToQuasiIso.Qh_inverts_quasiIso, instHasTwoOutOfThreePropertyQuasiIso, HomologicalComplexUpToQuasiIso.instIsLocalizationHomotopyCategoryQhQuasiIso, CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoFactorsh_hom_app, ComplexShape.QFactorsThroughHomotopy.areEqualizedByLocalization, homologyFunctor_inverts_quasiIso, HomotopyCategory.quotient_map_mem_quasiIso_iff, HomologicalComplexUpToQuasiIso.isIso_Q_map_iff_mem_quasiIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instHasTwoOutOfThreePropertyQuasiIso 📖	mathematical	—	CategoryTheory.MorphismProperty.HasTwoOutOfThreeProperty HomologicalComplex instCategory quasiIso	—	CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition instIsMultiplicativeQuasiIso CategoryTheory.CategoryWithHomology.hasHomology mem_quasiIso_iff quasiIso_iff_comp_right quasiIso_iff_comp_left
instIsMultiplicativeQuasiIso 📖	mathematical	—	CategoryTheory.MorphismProperty.IsMultiplicative HomologicalComplex instCategory quasiIso	—	CategoryTheory.CategoryWithHomology.hasHomology mem_quasiIso_iff quasiIso_of_isIso CategoryTheory.IsIso.id quasiIso_comp
instIsStableUnderRetractsQuasiIso 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderRetracts HomologicalComplex instCategory quasiIso	—	CategoryTheory.CategoryWithHomology.hasHomology mem_quasiIso_iff quasiIso_of_retractArrow
instRespectsIsoQuasiIso 📖	mathematical	—	CategoryTheory.MorphismProperty.RespectsIso HomologicalComplex instCategory quasiIso	—	CategoryTheory.MorphismProperty.respectsIso_of_isStableUnderComposition CategoryTheory.MorphismProperty.HasTwoOutOfThreeProperty.toIsStableUnderComposition instHasTwoOutOfThreePropertyQuasiIso CategoryTheory.CategoryWithHomology.hasHomology mem_quasiIso_iff quasiIso_of_isIso
mem_quasiIso_iff 📖	mathematical	—	quasiIso QuasiIso CategoryTheory.CategoryWithHomology.hasHomology sc	—	—
quasiIsoAt_map_iff_of_preservesHomology 📖	mathematical	—	QuasiIsoAt CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj HomologicalComplex instCategory CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Functor.map	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.ShortComplex.quasiIso_map_iff_of_preservesLeftHomology CategoryTheory.ShortComplex.hasHomology_of_preserves' CategoryTheory.Functor.PreservesHomology.preservesLeftHomologyOf CategoryTheory.Functor.PreservesHomology.preservesRightHomologyOf
quasiIsoAt_map_of_preservesHomology 📖	mathematical	—	QuasiIsoAt CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj HomologicalComplex instCategory CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Functor.map	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive quasiIsoAt_iff CategoryTheory.ShortComplex.quasiIso_map_of_preservesLeftHomology CategoryTheory.ShortComplex.hasHomology_of_preserves' CategoryTheory.Functor.PreservesHomology.preservesLeftHomologyOf CategoryTheory.Functor.PreservesHomology.preservesRightHomologyOf
quasiIso_map_iff_of_preservesHomology 📖	mathematical	HasHomology CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj HomologicalComplex instCategory CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.Functor.preservesZeroMorphisms_of_additive	QuasiIso CategoryTheory.Functor.map	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive quasiIsoAt_map_iff_of_preservesHomology
quasiIso_map_of_preservesHomology 📖	mathematical	HasHomology CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj HomologicalComplex instCategory CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.Functor.preservesZeroMorphisms_of_additive	QuasiIso CategoryTheory.Functor.map	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive quasiIsoAt_map_of_preservesHomology QuasiIso.quasiIsoAt

HomotopyEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
quasiIsoAt_hom 📖	mathematical	—	QuasiIsoAt CategoryTheory.Preadditive.preadditiveHasZeroMorphisms hom	—	quasiIsoAt_iff CategoryTheory.ShortComplex.quasiIso_iff CategoryTheory.Iso.isIso_hom
quasiIsoAt_inv 📖	mathematical	—	QuasiIsoAt CategoryTheory.Preadditive.preadditiveHasZeroMorphisms inv	—	quasiIsoAt_hom
quasiIso_hom 📖	mathematical	HomologicalComplex.HasHomology CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	QuasiIso hom	—	quasiIsoAt_hom
quasiIso_inv 📖	mathematical	HomologicalComplex.HasHomology CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	QuasiIso inv	—	quasiIsoAt_inv

QuasiIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
quasiIsoAt 📖	mathematical	HomologicalComplex.HasHomology	QuasiIsoAt	—	—

QuasiIsoAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
quasiIso 📖	mathematical	—	CategoryTheory.ShortComplex.QuasiIso CategoryTheory.Functor.obj HomologicalComplex HomologicalComplex.instCategory CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory HomologicalComplex.shortComplexFunctor CategoryTheory.Functor.map	—	—

(root)

Definitions

Name	Category	Theorems
QuasiIsoAt 📖	CompData	38 math math: quasiIsoAt_iff_comp_right, quasiIsoAt_iff_exactAt, CochainComplex.quasiIso_truncLEMap_iff, HomologicalComplex.quasiIsoAt_extendMap_iff, HomologicalComplex.instQuasiIsoAtιTruncLEF, HomologicalComplex.instQuasiIsoAtMapOppositeSymmUnopFunctorOp, QuasiIso.quasiIsoAt, quasiIsoAt_comp, HomotopyEquiv.quasiIsoAt_inv, HomologicalComplex.truncLE'.quasiIsoAt_truncLE'ToRestriction, HomologicalComplex.quasiIsoAt_unopFunctor_map_iff, ChainComplex.quasiIsoAt₀_iff, HomologicalComplex.instQuasiIsoAtOppositeMapSymmOpFunctorOp, CochainComplex.quasiIso_truncGEMap_iff, quasiIsoAt_of_comp_right, HomologicalComplex.quasiIsoAt_shortComplexTruncLE_g, CochainComplex.quasiIsoAt_shift_iff, HomologicalComplex.quasiIsoAt_πTruncGE, quasiIso_iff, quasiIsoAt_iff_isIso_homologyMap, HomologicalComplex.quasiIsoAt_iff_evaluation, quasiIsoAt_iff', CochainComplex.quasiIsoAt₀_iff, HomologicalComplex.truncGE'.quasiIsoAt_restrictionToTruncGE', quasiIsoAt_of_retract, HomologicalComplex.quasiIsoAt_ιTruncLE, quasiIsoAt_iff_comp_left, HomotopyEquiv.quasiIsoAt_hom, HomologicalComplex.quasiIso_truncGEMap_iff, quasiIsoAt_iff, HomologicalComplex.quasiIsoAt_map_of_preservesHomology, quasiIsoAt_of_comp_left, quasiIsoAt_iff_exactAt', HomologicalComplex.quasiIsoAt_opFunctor_map_iff, quasiIsoAt_of_isIso, HomologicalComplex.instQuasiIsoAtπTruncGEF, HomologicalComplex.quasiIso_truncLEMap_iff, HomologicalComplex.quasiIsoAt_map_iff_of_preservesHomology
isoOfQuasiIsoAt 📖	CompOp	5 math math: isoOfQuasiIsoAt_hom, isoOfQuasiIsoAt_hom_inv_id, isoOfQuasiIsoAt_inv_hom_id, isoOfQuasiIsoAt_inv_hom_id_assoc, isoOfQuasiIsoAt_hom_inv_id_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exactAt_iff_of_quasiIsoAt 📖	mathematical	—	HomologicalComplex.ExactAt	—	quasiIsoAt_iff_exactAt quasiIsoAt_iff_exactAt'
homotopyEquivalences_le_quasiIso 📖	mathematical	—	CategoryTheory.MorphismProperty HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra HomologicalComplex.homotopyEquivalences HomologicalComplex.quasiIso	—	CategoryTheory.CategoryWithHomology.hasHomology HomotopyEquiv.quasiIso_hom
instIsIsoHomologyMapOfQuasiIsoAt 📖	mathematical	—	CategoryTheory.IsIso HomologicalComplex.homology HomologicalComplex.homologyMap	—	—
isoOfQuasiIsoAt_hom 📖	mathematical	—	CategoryTheory.Iso.hom HomologicalComplex.homology isoOfQuasiIsoAt HomologicalComplex.homologyMap	—	—
isoOfQuasiIsoAt_hom_inv_id 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.homology HomologicalComplex.homologyMap CategoryTheory.Iso.inv isoOfQuasiIsoAt CategoryTheory.CategoryStruct.id	—	CategoryTheory.Iso.hom_inv_id
isoOfQuasiIsoAt_hom_inv_id_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.homology HomologicalComplex.homologyMap CategoryTheory.Iso.inv isoOfQuasiIsoAt	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' isoOfQuasiIsoAt_hom_inv_id
isoOfQuasiIsoAt_inv_hom_id 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.homology CategoryTheory.Iso.inv isoOfQuasiIsoAt HomologicalComplex.homologyMap CategoryTheory.CategoryStruct.id	—	CategoryTheory.Iso.inv_hom_id
isoOfQuasiIsoAt_inv_hom_id_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.homology CategoryTheory.Iso.inv isoOfQuasiIsoAt HomologicalComplex.homologyMap	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' isoOfQuasiIsoAt_inv_hom_id
quasiIsoAt_comp 📖	mathematical	—	QuasiIsoAt CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory	—	quasiIsoAt_iff CategoryTheory.Functor.map_comp CategoryTheory.ShortComplex.quasiIso_comp
quasiIsoAt_iff 📖	mathematical	—	QuasiIsoAt CategoryTheory.ShortComplex.QuasiIso CategoryTheory.Functor.obj HomologicalComplex HomologicalComplex.instCategory CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory HomologicalComplex.shortComplexFunctor CategoryTheory.Functor.map	—	QuasiIsoAt.quasiIso
quasiIsoAt_iff' 📖	mathematical	ComplexShape.prev ComplexShape.next	QuasiIsoAt CategoryTheory.ShortComplex.QuasiIso CategoryTheory.Functor.obj HomologicalComplex HomologicalComplex.instCategory CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory HomologicalComplex.shortComplexFunctor' CategoryTheory.Functor.map	—	quasiIsoAt_iff CategoryTheory.ShortComplex.quasiIso_iff_of_arrow_mk_iso
quasiIsoAt_iff_comp_left 📖	mathematical	—	QuasiIsoAt CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory	—	quasiIsoAt_of_comp_left quasiIsoAt_comp
quasiIsoAt_iff_comp_right 📖	mathematical	—	QuasiIsoAt CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory	—	quasiIsoAt_of_comp_right quasiIsoAt_comp
quasiIsoAt_iff_exactAt 📖	mathematical	HomologicalComplex.ExactAt	QuasiIsoAt	—	CategoryTheory.Limits.IsZero.of_iso CategoryTheory.Limits.IsZero.eq_of_src CategoryTheory.Limits.IsZero.eq_of_tgt
quasiIsoAt_iff_exactAt' 📖	mathematical	HomologicalComplex.ExactAt	QuasiIsoAt	—	CategoryTheory.Limits.IsZero.of_iso CategoryTheory.Limits.IsZero.eq_of_src CategoryTheory.Limits.IsZero.eq_of_tgt
quasiIsoAt_iff_isIso_homologyMap 📖	mathematical	—	QuasiIsoAt CategoryTheory.IsIso HomologicalComplex.homology HomologicalComplex.homologyMap	—	quasiIsoAt_iff CategoryTheory.ShortComplex.quasiIso_iff
quasiIsoAt_of_comp_left 📖	mathematical	—	QuasiIsoAt	—	quasiIsoAt_iff_isIso_homologyMap CategoryTheory.IsIso.of_isIso_comp_left HomologicalComplex.homologyMap_comp
quasiIsoAt_of_comp_right 📖	mathematical	—	QuasiIsoAt	—	quasiIsoAt_iff_isIso_homologyMap CategoryTheory.IsIso.of_isIso_comp_right HomologicalComplex.homologyMap_comp
quasiIsoAt_of_isIso 📖	mathematical	—	QuasiIsoAt	—	quasiIsoAt_iff CategoryTheory.ShortComplex.quasiIso_of_isIso CategoryTheory.Functor.map_isIso
quasiIsoAt_of_retract 📖	mathematical	—	QuasiIsoAt	—	quasiIsoAt_iff CategoryTheory.ShortComplex.quasiIso_of_retract
quasiIso_comp 📖	mathematical	HomologicalComplex.HasHomology	QuasiIso CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory	—	quasiIsoAt_comp QuasiIso.quasiIsoAt
quasiIso_iff 📖	mathematical	HomologicalComplex.HasHomology	QuasiIso QuasiIsoAt	—	QuasiIso.quasiIsoAt
quasiIso_iff_comp_left 📖	mathematical	HomologicalComplex.HasHomology	QuasiIso CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory	—	quasiIsoAt_iff_comp_left QuasiIso.quasiIsoAt
quasiIso_iff_comp_right 📖	mathematical	HomologicalComplex.HasHomology	QuasiIso CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory	—	quasiIsoAt_iff_comp_right QuasiIso.quasiIsoAt
quasiIso_iff_of_arrow_mk_iso 📖	mathematical	HomologicalComplex.HasHomology	QuasiIso	—	quasiIso_iff_comp_left quasiIso_of_isIso CategoryTheory.Arrow.isIso_left CategoryTheory.Iso.isIso_inv QuasiIso.congr_simp CategoryTheory.Arrow.w_mk_right quasiIso_iff_comp_right CategoryTheory.Arrow.isIso_right
quasiIso_of_arrow_mk_iso 📖	mathematical	HomologicalComplex.HasHomology	QuasiIso	—	quasiIso_iff_of_arrow_mk_iso
quasiIso_of_comp_left 📖	mathematical	HomologicalComplex.HasHomology	QuasiIso	—	quasiIso_iff_comp_left
quasiIso_of_comp_right 📖	mathematical	HomologicalComplex.HasHomology	QuasiIso	—	quasiIso_iff_comp_right
quasiIso_of_isIso 📖	mathematical	HomologicalComplex.HasHomology	QuasiIso	—	quasiIsoAt_of_isIso
quasiIso_of_retractArrow 📖	mathematical	HomologicalComplex.HasHomology	QuasiIso	—	quasiIsoAt_of_retract QuasiIso.quasiIsoAt

---

← Back to Index