Documentation Verification Report

Constructor

📁 Source: Mathlib/CategoryTheory/Localization/DerivabilityStructure/Constructor.lean

Statistics

Metric	Count
Definitions `fromRightResolution`	1
Theorems `mk'`, `fromRightResolution_map`, `fromRightResolution_obj`, `isConnected`, `mk'`	5
Total	6

CategoryTheory.LocalizerMorphism.IsLeftDerivabilityStructure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mk'` 📖	mathematical	`CategoryTheory.IsConnected` `CategoryTheory.LocalizerMorphism.LeftResolution` `CategoryTheory.LocalizerMorphism.LeftResolution.instCategory` `CategoryTheory.LocalizerMorphism.HasLeftResolutions` `CategoryTheory.Arrow` `CategoryTheory.instCategoryArrow` `CategoryTheory.MorphismProperty.arrow` `CategoryTheory.LocalizerMorphism.arrow`	`CategoryTheory.LocalizerMorphism.IsLeftDerivabilityStructure`	—	`CategoryTheory.LocalizerMorphism.isLeftDerivabilityStructure_iff_op` `CategoryTheory.CommaMorphism.w` `CategoryTheory.LocalizerMorphism.LeftResolution.hw` `CategoryTheory.isConnected_of_equivalent` `CategoryTheory.isConnected_op` `CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.mk'` `CategoryTheory.MorphismProperty.ContainsIdentities.op` `CategoryTheory.LocalizerMorphism.instIsLocalizedEquivalenceOppositeOpOp`

CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mk'` 📖	mathematical	`CategoryTheory.IsConnected` `CategoryTheory.LocalizerMorphism.RightResolution` `CategoryTheory.LocalizerMorphism.RightResolution.instCategory` `CategoryTheory.LocalizerMorphism.HasRightResolutions` `CategoryTheory.Arrow` `CategoryTheory.instCategoryArrow` `CategoryTheory.MorphismProperty.arrow` `CategoryTheory.LocalizerMorphism.arrow`	`CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure`	—	`CategoryTheory.LocalizerMorphism.isRightDerivabilityStructure_iff` `CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.isLocalization` `CategoryTheory.Functor.q_isLocalization` `CategoryTheory.IsConnected.is_nonempty` `CategoryTheory.TwoSquare.guitartExact_iff_isConnected_downwards` `Constructor.isConnected`

CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.Constructor

Definitions

Name	Category	Theorems
`fromRightResolution` 📖	CompOp	2 math math: `fromRightResolution_map`, `fromRightResolution_obj`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fromRightResolution_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.LocalizerMorphism.RightResolution` `CategoryTheory.LocalizerMorphism.RightResolution.instCategory` `CategoryTheory.TwoSquare.CostructuredArrowDownwards` `CategoryTheory.LocalizerMorphism.functor` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.id` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.rightUnitor` `CategoryTheory.instCategoryCostructuredArrow` `CategoryTheory.StructuredArrow` `CategoryTheory.instCategoryStructuredArrow` `CategoryTheory.Functor.obj` `CategoryTheory.TwoSquare.structuredArrowDownwards` `fromRightResolution` `CategoryTheory.CostructuredArrow.homMk` `CategoryTheory.LocalizerMorphism.RightResolution.X₁` `CategoryTheory.LocalizerMorphism.RightResolution.w` `CategoryTheory.StructuredArrow.homMk` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Comma.right` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Localization.isoOfHom` `CategoryTheory.LocalizerMorphism.RightResolution.hw` `CategoryTheory.Comma.left` `CategoryTheory.LocalizerMorphism.RightResolution.Hom.f`	—	`CategoryTheory.LocalizerMorphism.RightResolution.hw`
`fromRightResolution_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.LocalizerMorphism.RightResolution` `CategoryTheory.LocalizerMorphism.RightResolution.instCategory` `CategoryTheory.TwoSquare.CostructuredArrowDownwards` `CategoryTheory.LocalizerMorphism.functor` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.id` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.rightUnitor` `CategoryTheory.instCategoryCostructuredArrow` `CategoryTheory.StructuredArrow` `CategoryTheory.instCategoryStructuredArrow` `CategoryTheory.TwoSquare.structuredArrowDownwards` `fromRightResolution` `CategoryTheory.LocalizerMorphism.RightResolution.X₁` `CategoryTheory.LocalizerMorphism.RightResolution.w` `CategoryTheory.StructuredArrow.homMk` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Comma.right` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Localization.isoOfHom` `CategoryTheory.LocalizerMorphism.RightResolution.hw`	—	—
`isConnected` 📖	mathematical	`CategoryTheory.IsConnected` `CategoryTheory.LocalizerMorphism.RightResolution` `CategoryTheory.LocalizerMorphism.RightResolution.instCategory` `CategoryTheory.LocalizerMorphism.HasRightResolutions` `CategoryTheory.Arrow` `CategoryTheory.instCategoryArrow` `CategoryTheory.MorphismProperty.arrow` `CategoryTheory.LocalizerMorphism.arrow`	`CategoryTheory.TwoSquare.CostructuredArrowDownwards` `CategoryTheory.LocalizerMorphism.functor` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.id` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.rightUnitor` `CategoryTheory.instCategoryCostructuredArrow` `CategoryTheory.StructuredArrow` `CategoryTheory.instCategoryStructuredArrow` `CategoryTheory.Functor.obj` `CategoryTheory.TwoSquare.structuredArrowDownwards`	—	`CategoryTheory.IsConnected.is_nonempty` `CategoryTheory.TwoSquare.CostructuredArrowDownwards.mk_surjective` `CategoryTheory.LocalizerMorphism.RightResolution.hw` `CategoryTheory.Category.id_comp` `CategoryTheory.MorphismProperty.id_mem` `CategoryTheory.zigzag_obj_of_zigzag` `CategoryTheory.isPreconnected_zigzag` `CategoryTheory.IsConnected.toIsPreconnected` `CategoryTheory.Zigzag.trans` `CategoryTheory.Zigzag.of_hom` `CategoryTheory.Localization.isoOfHom_id_inv` `CategoryTheory.Category.comp_id` `CategoryTheory.StructuredArrow.homMk.congr_simp` `CategoryTheory.Zigzag.of_inv` `CategoryTheory.Arrow.w_mk_right` `CategoryTheory.StructuredArrow.hom_ext` `CategoryTheory.cancel_epi` `CategoryTheory.epi_of_strongEpi` `CategoryTheory.strongEpi_of_isIso` `CategoryTheory.Iso.isIso_hom` `CategoryTheory.Localization.isoOfHom_hom` `CategoryTheory.Localization.isoOfHom_hom_inv_id_assoc` `CategoryTheory.Functor.map_comp_assoc` `CategoryTheory.Arrow.mk_hom` `CategoryTheory.Functor.map_comp` `CategoryTheory.Category.assoc` `CategoryTheory.zigzag_isConnected` `CategoryTheory.Zigzag.symm`

---

← Back to Index