Documentation Verification Report

NReflectsIso

📁 Source: Mathlib/AlgebraicTopology/DoldKan/NReflectsIso.lean

Statistics

Metric	Count
Definitions	0
Theorems `compatibility_N₂_N₁_karoubi`, `instReflectsIsomorphismsKaroubiSimplicialObjectChainComplexNatN₂`, `instReflectsIsomorphismsSimplicialObjectKaroubiChainComplexNatN₁`	3
Total	3

AlgebraicTopology.DoldKan

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compatibility_N₂_N₁_karoubi` 📖	mathematical	—	`CategoryTheory.Functor.comp` `CategoryTheory.Idempotents.Karoubi` `CategoryTheory.SimplicialObject` `CategoryTheory.instCategorySimplicialObject` `CategoryTheory.Idempotents.Karoubi.instCategory` `ChainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Nat.instOne` `HomologicalComplex.instCategory` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Idempotents.instPreadditiveKaroubi` `N₂` `CategoryTheory.Equivalence.functor` `CategoryTheory.Idempotents.karoubiChainComplexEquivalence` `CategoryTheory.Functor` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.Functor.category` `HomologicalComplex` `CategoryTheory.Idempotents.karoubiFunctorCategoryEmbedding` `N₁` `CategoryTheory.Functor.mapHomologicalComplex` `CategoryTheory.Equivalence.inverse` `CategoryTheory.Idempotents.KaroubiKaroubi.equivalence` `CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `CategoryTheory.Idempotents.KaroubiKaroubi.equivalence.additive_inverse`	—	`CategoryTheory.Functor.ext` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `CategoryTheory.Idempotents.KaroubiKaroubi.equivalence.additive_inverse` `HomologicalComplex.ext` `CategoryTheory.Idempotents.Karoubi.ext` `CategoryTheory.Category.comp_id` `karoubi_PInfty_f` `PInfty_f_naturality` `CategoryTheory.Category.id_comp` `CategoryTheory.Idempotents.Karoubi.hom_ext` `HomologicalComplex.Hom.comm` `CategoryTheory.Category.assoc` `CategoryTheory.Idempotents.Karoubi.eqToHom_f` `AlgebraicTopology.karoubi_alternatingFaceMapComplex_d` `CategoryTheory.Idempotents.app_idem_assoc` `HomologicalComplex.hom_ext` `HomologicalComplex.eqToHom_f` `CategoryTheory.Idempotents.app_p_comp` `PInfty_f_naturality_assoc` `CategoryTheory.Idempotents.app_comp_p` `PInfty_f_idem_assoc`
`instReflectsIsomorphismsKaroubiSimplicialObjectChainComplexNatN₂` 📖	mathematical	—	`CategoryTheory.Functor.ReflectsIsomorphisms` `CategoryTheory.Idempotents.Karoubi` `CategoryTheory.SimplicialObject` `CategoryTheory.instCategorySimplicialObject` `CategoryTheory.Idempotents.Karoubi.instCategory` `ChainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Nat.instOne` `HomologicalComplex.instCategory` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `N₂`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `CategoryTheory.Idempotents.KaroubiKaroubi.equivalence.additive_inverse` `compatibility_N₂_N₁_karoubi` `CategoryTheory.Functor.comp_map` `CategoryTheory.Functor.map_isIso` `CategoryTheory.isIso_of_reflects_iso` `CategoryTheory.reflectsIsomorphisms_comp` `CategoryTheory.reflectsIsomorphisms_of_full_and_faithful` `CategoryTheory.Idempotents.instFullKaroubiFunctorKaroubiFunctorCategoryEmbedding` `CategoryTheory.Idempotents.instFaithfulKaroubiFunctorKaroubiFunctorCategoryEmbedding` `instReflectsIsomorphismsSimplicialObjectKaroubiChainComplexNatN₁` `CategoryTheory.Equivalence.full_functor` `CategoryTheory.Equivalence.faithful_functor` `CategoryTheory.Functor.mapHomologicalComplex_reflects_iso` `CategoryTheory.Equivalence.full_inverse` `CategoryTheory.Equivalence.faithful_inverse`
`instReflectsIsomorphismsSimplicialObjectKaroubiChainComplexNatN₁` 📖	mathematical	—	`CategoryTheory.Functor.ReflectsIsomorphisms` `CategoryTheory.SimplicialObject` `CategoryTheory.instCategorySimplicialObject` `CategoryTheory.Idempotents.Karoubi` `ChainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Nat.instOne` `HomologicalComplex.instCategory` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Idempotents.Karoubi.instCategory` `N₁`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `HomologicalComplex.congr_hom` `CategoryTheory.Idempotents.Karoubi.hom_ext_iff` `CategoryTheory.IsIso.hom_inv_id` `CategoryTheory.IsIso.inv_hom_id` `CategoryTheory.Idempotents.Karoubi.HomologicalComplex.p_comm_f_assoc` `CategoryTheory.Category.assoc` `CategoryTheory.Category.id_comp` `PInfty_f_naturality_assoc` `CategoryTheory.IsIso.hom_inv_id_assoc` `CategoryTheory.SimplicialObject.σ_naturality` `CategoryTheory.IsIso.inv_hom_id_assoc` `CategoryTheory.NatIso.isIso_of_isIso_app`

---

← Back to Index