Basic

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

Statistics

Metric	Count
Definitions IsLeftDerivabilityStructure, IsRightDerivabilityStructure	2
Theorems guitartExact', hasLeftResolutions, guitartExact', hasRightResolutions, guitartExact_of_isLeftDerivabilityStructure, guitartExact_of_isLeftDerivabilityStructure', guitartExact_of_isRightDerivabilityStructure, guitartExact_of_isRightDerivabilityStructure', instHasLeftResolutionsIdOfContainsIdentities, instHasRightResolutionsIdOfContainsIdentities, instIsLeftDerivabilityStructureIdOfContainsIdentities, instIsRightDerivabilityStructureIdOfContainsIdentities, isLeftDerivabilityStructure_iff, isLeftDerivabilityStructure_iff_op, isRightDerivabilityStructure_iff	15
Total	17

CategoryTheory.LocalizerMorphism

Definitions

Name	Category	Theorems
IsLeftDerivabilityStructure 📖	CompData	5 math math: IsLeftDerivabilityStructure.mk', instIsLeftDerivabilityStructureIdOfContainsIdentities, HomotopicalAlgebra.CofibrantObject.instIsLeftDerivabilityStructureWeakEquivalencesLocalizerMorphism, isLeftDerivabilityStructure_iff, isLeftDerivabilityStructure_iff_op
IsRightDerivabilityStructure 📖	CompData	6 math math: IsRightDerivabilityStructure.mk', isRightDerivabilityStructure_of_functorial_resolutions, isRightDerivabilityStructure_iff, instIsRightDerivabilityStructureIdOfContainsIdentities, HomotopicalAlgebra.FibrantObject.instIsRightDerivabilityStructureWeakEquivalencesLocalizerMorphism, isLeftDerivabilityStructure_iff_op

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
guitartExact_of_isLeftDerivabilityStructure 📖	mathematical	—	CategoryTheory.TwoSquare.GuitartExact functor localizedFunctor CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.CatCommSq.iso catCommSq	—	guitartExact_of_isLeftDerivabilityStructure'
guitartExact_of_isLeftDerivabilityStructure' 📖	mathematical	—	CategoryTheory.TwoSquare.GuitartExact functor CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp	—	isLeftDerivabilityStructure_iff IsLeftDerivabilityStructure.hasLeftResolutions
guitartExact_of_isRightDerivabilityStructure 📖	mathematical	—	CategoryTheory.TwoSquare.GuitartExact functor localizedFunctor CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.CatCommSq.iso catCommSq	—	guitartExact_of_isRightDerivabilityStructure'
guitartExact_of_isRightDerivabilityStructure' 📖	mathematical	—	CategoryTheory.TwoSquare.GuitartExact functor CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp	—	isRightDerivabilityStructure_iff IsRightDerivabilityStructure.hasRightResolutions
instHasLeftResolutionsIdOfContainsIdentities 📖	mathematical	—	HasLeftResolutions id	—	CategoryTheory.MorphismProperty.id_mem
instHasRightResolutionsIdOfContainsIdentities 📖	mathematical	—	HasRightResolutions id	—	CategoryTheory.MorphismProperty.id_mem
instIsLeftDerivabilityStructureIdOfContainsIdentities 📖	mathematical	—	IsLeftDerivabilityStructure id	—	isLeftDerivabilityStructure_iff CategoryTheory.Functor.q_isLocalization instHasLeftResolutionsIdOfContainsIdentities CategoryTheory.TwoSquare.guitartExact_id'
instIsRightDerivabilityStructureIdOfContainsIdentities 📖	mathematical	—	IsRightDerivabilityStructure id	—	isRightDerivabilityStructure_iff CategoryTheory.Functor.q_isLocalization instHasRightResolutionsIdOfContainsIdentities CategoryTheory.TwoSquare.guitartExact_id
isLeftDerivabilityStructure_iff 📖	mathematical	HasLeftResolutions	IsLeftDerivabilityStructure CategoryTheory.TwoSquare.GuitartExact functor CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp	—	isLeftDerivabilityStructure_iff_op isRightDerivabilityStructure_iff CategoryTheory.Functor.IsLocalization.op instHasRightResolutionsOppositeOpOpOfHasLeftResolutions CategoryTheory.TwoSquare.guitartExact_op_iff
isLeftDerivabilityStructure_iff_op 📖	mathematical	—	IsLeftDerivabilityStructure IsRightDerivabilityStructure Opposite CategoryTheory.Category.opposite CategoryTheory.MorphismProperty.op CategoryTheory.Category.toCategoryStruct op	—	CategoryTheory.Functor.q_isLocalization CategoryTheory.TwoSquare.guitartExact_op_iff isRightDerivabilityStructure_iff CategoryTheory.Localization.isLocalization_op instHasRightResolutionsOppositeOpOpOfHasLeftResolutions hasLeftResolutions_iff_op IsRightDerivabilityStructure.hasRightResolutions guitartExact_of_isRightDerivabilityStructure'
isRightDerivabilityStructure_iff 📖	mathematical	HasRightResolutions	IsRightDerivabilityStructure CategoryTheory.TwoSquare.GuitartExact functor CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp	—	CategoryTheory.Functor.q_isLocalization IsRightDerivabilityStructure.guitartExact' CategoryTheory.TwoSquare.ext CategoryTheory.TwoSquare.vComp'_app CategoryTheory.Localization.liftNatIso_hom CategoryTheory.Localization.liftNatTrans_app CategoryTheory.Category.id_comp CategoryTheory.Category.assoc CategoryTheory.Functor.map_id CategoryTheory.Functor.map_comp CategoryTheory.Iso.inv_hom_id_app CategoryTheory.Category.comp_id CategoryTheory.Functor.map_comp_assoc CategoryTheory.Iso.inv_hom_id_app_assoc CategoryTheory.TwoSquare.GuitartExact.vComp'_iff_of_equivalences

CategoryTheory.LocalizerMorphism.IsLeftDerivabilityStructure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
guitartExact' 📖	mathematical	—	CategoryTheory.TwoSquare.GuitartExact CategoryTheory.MorphismProperty.Localization CategoryTheory.MorphismProperty.instCategoryLocalization CategoryTheory.MorphismProperty.Q CategoryTheory.LocalizerMorphism.functor CategoryTheory.LocalizerMorphism.localizedFunctor CategoryTheory.Functor.q_isLocalization CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.CatCommSq.iso CategoryTheory.LocalizerMorphism.catCommSq	—	—
hasLeftResolutions 📖	mathematical	—	CategoryTheory.LocalizerMorphism.HasLeftResolutions	—	—

CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
guitartExact' 📖	mathematical	—	CategoryTheory.TwoSquare.GuitartExact CategoryTheory.MorphismProperty.Localization CategoryTheory.MorphismProperty.instCategoryLocalization CategoryTheory.LocalizerMorphism.functor CategoryTheory.MorphismProperty.Q CategoryTheory.LocalizerMorphism.localizedFunctor CategoryTheory.Functor.q_isLocalization CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.CatCommSq.iso CategoryTheory.LocalizerMorphism.catCommSq	—	—
hasRightResolutions 📖	mathematical	—	CategoryTheory.LocalizerMorphism.HasRightResolutions	—	—

---

← Back to Index