OfFunctorialResolutions

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

Statistics

Metric	Count
Definitions localizerMorphismInv, ι	2
Theorems W₁_ι_app, localizerMorphismInv_functor, Φ_functor_map_ι_app, hasRightResolutions_arrow_of_functorial_resolutions, isConnected_rightResolution_of_functorial_resolutions, isLocalizedEquivalence_of_functorial_right_resolutions, isRightDerivabilityStructure_of_functorial_resolutions	7
Total	9

CategoryTheory.LocalizerMorphism

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasRightResolutions_arrow_of_functorial_resolutions 📖	mathematical	CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Functor.comp functor CategoryTheory.NatTrans.app	HasRightResolutions CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.MorphismProperty.arrow arrow	—	CategoryTheory.NatTrans.naturality
isConnected_rightResolution_of_functorial_resolutions 📖	mathematical	CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Functor.comp functor CategoryTheory.NatTrans.app CategoryTheory.MorphismProperty.inverseImage	CategoryTheory.IsConnected RightResolution RightResolution.instCategory	—	CategoryTheory.MorphismProperty.IsMultiplicative.instInverseImage CategoryTheory.zigzag_isPreconnected CategoryTheory.MorphismProperty.comp_mem CategoryTheory.MorphismProperty.HasTwoOutOfThreeProperty.toIsStableUnderComposition RightResolution.hw CategoryTheory.Zigzag.of_hom functorialRightResolutions.Φ_functor_map_ι_app CategoryTheory.Zigzag.of_inv CategoryTheory.NatTrans.naturality
isLocalizedEquivalence_of_functorial_right_resolutions 📖	mathematical	CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Functor.comp functor CategoryTheory.NatTrans.app CategoryTheory.MorphismProperty.inverseImage	IsLocalizedEquivalence	—	isLocalizedEquivalence_of_unit_of_unit functorialRightResolutions.W₁_ι_app
isRightDerivabilityStructure_of_functorial_resolutions 📖	mathematical	CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Functor.comp functor CategoryTheory.NatTrans.app CategoryTheory.MorphismProperty.inverseImage	IsRightDerivabilityStructure	—	CategoryTheory.MorphismProperty.IsMultiplicative.instInverseImage isLocalizedEquivalence_of_functorial_right_resolutions hasRightResolutions_arrow_of_functorial_resolutions isConnected_rightResolution_of_functorial_resolutions IsRightDerivabilityStructure.mk' CategoryTheory.MorphismProperty.IsMultiplicative.toContainsIdentities

CategoryTheory.LocalizerMorphism.functorialRightResolutions

Definitions

Name	Category	Theorems
localizerMorphismInv 📖	CompOp	1 math math: localizerMorphismInv_functor
ι 📖	CompOp	2 math math: W₁_ι_app, Φ_functor_map_ι_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
W₁_ι_app 📖	mathematical	CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.LocalizerMorphism.functor CategoryTheory.NatTrans.app CategoryTheory.MorphismProperty.inverseImage	ι	—	Φ_functor_map_ι_app
localizerMorphismInv_functor 📖	mathematical	CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.LocalizerMorphism.functor CategoryTheory.NatTrans.app CategoryTheory.MorphismProperty.inverseImage	localizerMorphismInv	—	—
Φ_functor_map_ι_app 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.LocalizerMorphism.functor CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.NatTrans.app ι	—	CategoryTheory.NatTrans.congr_app CategoryTheory.Functor.full_whiskeringRight_obj CategoryTheory.Functor.map_preimage

---

← Back to Index