Documentation Verification Report

Resolution

📁 Source: Mathlib/CategoryTheory/Localization/Resolution.lean

Statistics

Metric	Count
Definitions `HasLeftResolutions`, `HasRightResolutions`, `comp`, `f`, `id`, `X₁`, `instCategory`, `op`, `opEquivalence`, `opFunctor`, `unop`, `w`, `RightResolution`, `comp`, `f`, `id`, `X₁`, `instCategory`, `op`, `unop`, `unopFunctor`, `w`	22
Theorems `comm`, `comm_assoc`, `comp_f`, `ext`, `ext_iff`, `id_f`, `comp_f`, `comp_f_assoc`, `hom_ext`, `hom_ext_iff`, `hw`, `id_f`, `mk_surjective`, `opEquivalence_counitIso`, `opEquivalence_functor`, `opEquivalence_inverse`, `opEquivalence_unitIso`, `opFunctor_map_f`, `opFunctor_obj`, `op_X₁`, `op_w`, `unop_X₁`, `unop_w`, `comm`, `comm_assoc`, `comp_f`, `ext`, `ext_iff`, `id_f`, `comp_f`, `comp_f_assoc`, `hom_ext`, `hom_ext_iff`, `hw`, `id_f`, `mk_surjective`, `op_X₁`, `op_w`, `unopFunctor_map_f`, `unopFunctor_obj`, `unop_X₁`, `unop_w`, `essSurj_of_hasLeftResolutions`, `essSurj_of_hasRightResolutions`, `hasLeftResolutions_iff_op`, `hasRightResolutions_iff_op`, `instHasLeftResolutionsOppositeOpOpOfHasRightResolutions`, `instHasRightResolutionsOppositeOpOpOfHasLeftResolutions`, `isIso_iff_of_hasLeftResolutions`, `isIso_iff_of_hasRightResolutions`, `nonempty_leftResolution_iff_op`, `nonempty_rightResolution_iff_op`	52
Total	74

CategoryTheory.LocalizerMorphism

Definitions

Name	Category	Theorems
`HasLeftResolutions` 📖	MathDef	6 math math: `hasLeftResolutions_iff_op`, `instHasLeftResolutionsOppositeOpOpOfHasRightResolutions`, `HomotopicalAlgebra.CofibrantObject.instHasLeftResolutionsArrowArrowWeakEquivalencesArrowLocalizerMorphism`, `IsLeftDerivabilityStructure.hasLeftResolutions`, `instHasLeftResolutionsIdOfContainsIdentities`, `hasRightResolutions_iff_op`
`HasRightResolutions` 📖	MathDef	7 math math: `IsRightDerivabilityStructure.hasRightResolutions`, `hasRightResolutions_arrow_of_functorial_resolutions`, `hasLeftResolutions_iff_op`, `HomotopicalAlgebra.FibrantObject.instHasRightResolutionsArrowArrowWeakEquivalencesArrowLocalizerMorphism`, `instHasRightResolutionsIdOfContainsIdentities`, `hasRightResolutions_iff_op`, `instHasRightResolutionsOppositeOpOpOfHasLeftResolutions`
`RightResolution` 📖	CompData	17 math math: `LeftResolution.opFunctor_map_f`, `IsRightDerivabilityStructure.Constructor.fromRightResolution_map`, `RightResolution.comp_f_assoc`, `LeftResolution.opEquivalence_unitIso`, `nonempty_rightResolution_iff_op`, `LeftResolution.opEquivalence_inverse`, `LeftResolution.opFunctor_obj`, `HomotopicalAlgebra.FibrantObject.instIsConnectedRightResolutionWeakEquivalencesLocalizerMorphism`, `RightResolution.id_f`, `RightResolution.unopFunctor_obj`, `RightResolution.comp_f`, `isConnected_rightResolution_of_functorial_resolutions`, `nonempty_leftResolution_iff_op`, `RightResolution.unopFunctor_map_f`, `LeftResolution.opEquivalence_counitIso`, `IsRightDerivabilityStructure.Constructor.fromRightResolution_obj`, `LeftResolution.opEquivalence_functor`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`essSurj_of_hasLeftResolutions` 📖	mathematical	`HasLeftResolutions`	`CategoryTheory.Functor.EssSurj` `CategoryTheory.Functor.comp` `functor`	—	`CategoryTheory.Localization.essSurj` `LeftResolution.hw`
`essSurj_of_hasRightResolutions` 📖	mathematical	`HasRightResolutions`	`CategoryTheory.Functor.EssSurj` `CategoryTheory.Functor.comp` `functor`	—	`CategoryTheory.Localization.essSurj` `RightResolution.hw`
`hasLeftResolutions_iff_op` 📖	mathematical	—	`HasLeftResolutions` `HasRightResolutions` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.MorphismProperty.op` `CategoryTheory.Category.toCategoryStruct` `op`	—	—
`hasRightResolutions_iff_op` 📖	mathematical	—	`HasRightResolutions` `HasLeftResolutions` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.MorphismProperty.op` `CategoryTheory.Category.toCategoryStruct` `op`	—	—
`instHasLeftResolutionsOppositeOpOpOfHasRightResolutions` 📖	mathematical	`HasRightResolutions`	`HasLeftResolutions` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.MorphismProperty.op` `CategoryTheory.Category.toCategoryStruct` `op`	—	`hasRightResolutions_iff_op`
`instHasRightResolutionsOppositeOpOpOfHasLeftResolutions` 📖	mathematical	`HasLeftResolutions`	`HasRightResolutions` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.MorphismProperty.op` `CategoryTheory.Category.toCategoryStruct` `op`	—	`hasLeftResolutions_iff_op`
`isIso_iff_of_hasLeftResolutions` 📖	mathematical	`HasLeftResolutions`	`CategoryTheory.IsIso` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.obj` `functor` `CategoryTheory.NatTrans.app`	—	`CategoryTheory.NatIso.isIso_app_of_isIso` `essSurj_of_hasLeftResolutions` `CategoryTheory.NatTrans.isIso_app_iff_of_iso` `CategoryTheory.NatIso.isIso_of_isIso_app`
`isIso_iff_of_hasRightResolutions` 📖	mathematical	`HasRightResolutions`	`CategoryTheory.IsIso` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.obj` `functor` `CategoryTheory.NatTrans.app`	—	`CategoryTheory.NatIso.isIso_app_of_isIso` `essSurj_of_hasRightResolutions` `CategoryTheory.NatTrans.isIso_app_iff_of_iso` `CategoryTheory.NatIso.isIso_of_isIso_app`
`nonempty_leftResolution_iff_op` 📖	mathematical	—	`LeftResolution` `RightResolution` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.MorphismProperty.op` `CategoryTheory.Category.toCategoryStruct` `op` `Opposite.op`	—	`Equiv.nonempty_congr`
`nonempty_rightResolution_iff_op` 📖	mathematical	—	`RightResolution` `LeftResolution` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.MorphismProperty.op` `CategoryTheory.Category.toCategoryStruct` `op` `Opposite.op`	—	`Equiv.nonempty_congr`

CategoryTheory.LocalizerMorphism.LeftResolution

Definitions

Name	Category	Theorems
`X₁` 📖	CompOp	16 math math: `opFunctor_map_f`, `id_f`, `CategoryTheory.LocalizerMorphism.RightResolution.op_X₁`, `Hom.id_f`, `unop_X₁`, `Hom.comm`, `CategoryTheory.LocalizerMorphism.RightResolution.unop_X₁`, `Hom.comp_f`, `unop_w`, `comp_f_assoc`, `comp_f`, `hw`, `HomotopicalAlgebra.CofibrantObject.instWeakEquivalenceWWeakEquivalences`, `op_w`, `op_X₁`, `Hom.comm_assoc`
`instCategory` 📖	CompOp	12 math math: `opFunctor_map_f`, `id_f`, `opEquivalence_unitIso`, `opEquivalence_inverse`, `opFunctor_obj`, `HomotopicalAlgebra.CofibrantObject.instIsConnectedLeftResolutionWeakEquivalencesLocalizerMorphism`, `comp_f_assoc`, `CategoryTheory.LocalizerMorphism.RightResolution.unopFunctor_obj`, `comp_f`, `CategoryTheory.LocalizerMorphism.RightResolution.unopFunctor_map_f`, `opEquivalence_counitIso`, `opEquivalence_functor`
`op` 📖	CompOp	4 math math: `opFunctor_map_f`, `opFunctor_obj`, `op_w`, `op_X₁`
`opEquivalence` 📖	CompOp	4 math math: `opEquivalence_unitIso`, `opEquivalence_inverse`, `opEquivalence_counitIso`, `opEquivalence_functor`
`opFunctor` 📖	CompOp	4 math math: `opFunctor_map_f`, `opFunctor_obj`, `opEquivalence_counitIso`, `opEquivalence_functor`
`unop` 📖	CompOp	2 math math: `unop_X₁`, `unop_w`
`w` 📖	CompOp	8 math math: `Hom.comm`, `unop_w`, `hw`, `HomotopicalAlgebra.CofibrantObject.instWeakEquivalenceWWeakEquivalences`, `CategoryTheory.LocalizerMorphism.RightResolution.unop_w`, `op_w`, `Hom.comm_assoc`, `CategoryTheory.LocalizerMorphism.RightResolution.op_w`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_f` 📖	mathematical	—	`Hom.f` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.LocalizerMorphism.LeftResolution` `CategoryTheory.Category.toCategoryStruct` `instCategory` `X₁`	—	—
`comp_f_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `X₁` `Hom.f` `CategoryTheory.LocalizerMorphism.LeftResolution` `instCategory`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `comp_f`
`hom_ext` 📖	—	`Hom.f`	—	—	`Hom.ext`
`hom_ext_iff` 📖	mathematical	—	`Hom.f`	—	`hom_ext`
`hw` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.LocalizerMorphism.functor` `X₁` `w`	—	—
`id_f` 📖	mathematical	—	`Hom.f` `CategoryTheory.CategoryStruct.id` `CategoryTheory.LocalizerMorphism.LeftResolution` `CategoryTheory.Category.toCategoryStruct` `instCategory` `X₁`	—	—
`mk_surjective` 📖	—	—	—	—	`hw`
`opEquivalence_counitIso` 📖	mathematical	—	`CategoryTheory.Equivalence.counitIso` `Opposite` `CategoryTheory.LocalizerMorphism.LeftResolution` `CategoryTheory.LocalizerMorphism.RightResolution` `CategoryTheory.Category.opposite` `CategoryTheory.MorphismProperty.op` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.LocalizerMorphism.op` `Opposite.op` `instCategory` `CategoryTheory.LocalizerMorphism.RightResolution.instCategory` `opEquivalence` `CategoryTheory.Iso.refl` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.rightOp` `Opposite.unop` `CategoryTheory.LocalizerMorphism.RightResolution.unopFunctor` `opFunctor`	—	—
`opEquivalence_functor` 📖	mathematical	—	`CategoryTheory.Equivalence.functor` `Opposite` `CategoryTheory.LocalizerMorphism.LeftResolution` `CategoryTheory.LocalizerMorphism.RightResolution` `CategoryTheory.Category.opposite` `CategoryTheory.MorphismProperty.op` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.LocalizerMorphism.op` `Opposite.op` `instCategory` `CategoryTheory.LocalizerMorphism.RightResolution.instCategory` `opEquivalence` `opFunctor`	—	—
`opEquivalence_inverse` 📖	mathematical	—	`CategoryTheory.Equivalence.inverse` `Opposite` `CategoryTheory.LocalizerMorphism.LeftResolution` `CategoryTheory.LocalizerMorphism.RightResolution` `CategoryTheory.Category.opposite` `CategoryTheory.MorphismProperty.op` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.LocalizerMorphism.op` `Opposite.op` `instCategory` `CategoryTheory.LocalizerMorphism.RightResolution.instCategory` `opEquivalence` `CategoryTheory.Functor.rightOp` `Opposite.unop` `CategoryTheory.LocalizerMorphism.RightResolution.unopFunctor`	—	—
`opEquivalence_unitIso` 📖	mathematical	—	`CategoryTheory.Equivalence.unitIso` `Opposite` `CategoryTheory.LocalizerMorphism.LeftResolution` `CategoryTheory.LocalizerMorphism.RightResolution` `CategoryTheory.Category.opposite` `CategoryTheory.MorphismProperty.op` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.LocalizerMorphism.op` `Opposite.op` `instCategory` `CategoryTheory.LocalizerMorphism.RightResolution.instCategory` `opEquivalence` `CategoryTheory.Iso.refl` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.id`	—	—
`opFunctor_map_f` 📖	mathematical	—	`CategoryTheory.LocalizerMorphism.RightResolution.Hom.f` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.MorphismProperty.op` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.LocalizerMorphism.op` `Opposite.op` `op` `Opposite.unop` `CategoryTheory.LocalizerMorphism.LeftResolution` `CategoryTheory.Functor.map` `instCategory` `CategoryTheory.LocalizerMorphism.RightResolution` `CategoryTheory.LocalizerMorphism.RightResolution.instCategory` `opFunctor` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `X₁` `Hom.f` `Quiver.Hom.unop`	—	—
`opFunctor_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.LocalizerMorphism.LeftResolution` `CategoryTheory.Category.opposite` `instCategory` `CategoryTheory.LocalizerMorphism.RightResolution` `CategoryTheory.MorphismProperty.op` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.LocalizerMorphism.op` `Opposite.op` `CategoryTheory.LocalizerMorphism.RightResolution.instCategory` `opFunctor` `op` `Opposite.unop`	—	—
`op_X₁` 📖	mathematical	—	`CategoryTheory.LocalizerMorphism.RightResolution.X₁` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.MorphismProperty.op` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.LocalizerMorphism.op` `Opposite.op` `op` `X₁`	—	—
`op_w` 📖	mathematical	—	`CategoryTheory.LocalizerMorphism.RightResolution.w` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.MorphismProperty.op` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.LocalizerMorphism.op` `Opposite.op` `op` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Functor.obj` `CategoryTheory.LocalizerMorphism.functor` `X₁` `w`	—	—
`unop_X₁` 📖	mathematical	—	`CategoryTheory.LocalizerMorphism.RightResolution.X₁` `Opposite.unop` `unop` `X₁` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.MorphismProperty.op` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.LocalizerMorphism.op`	—	—
`unop_w` 📖	mathematical	—	`CategoryTheory.LocalizerMorphism.RightResolution.w` `Opposite.unop` `unop` `Quiver.Hom.unop` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.LocalizerMorphism.functor` `CategoryTheory.MorphismProperty.op` `CategoryTheory.LocalizerMorphism.op` `X₁` `w`	—	—

CategoryTheory.LocalizerMorphism.LeftResolution.Hom

Definitions

Name	Category	Theorems
`comp` 📖	CompOp	1 math math: `comp_f`
`f` 📖	CompOp	11 math math: `CategoryTheory.LocalizerMorphism.LeftResolution.opFunctor_map_f`, `CategoryTheory.LocalizerMorphism.LeftResolution.id_f`, `id_f`, `comm`, `comp_f`, `CategoryTheory.LocalizerMorphism.LeftResolution.hom_ext_iff`, `CategoryTheory.LocalizerMorphism.LeftResolution.comp_f_assoc`, `CategoryTheory.LocalizerMorphism.LeftResolution.comp_f`, `ext_iff`, `CategoryTheory.LocalizerMorphism.RightResolution.unopFunctor_map_f`, `comm_assoc`
`id` 📖	CompOp	1 math math: `id_f`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comm` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.LocalizerMorphism.functor` `CategoryTheory.LocalizerMorphism.LeftResolution.X₁` `CategoryTheory.Functor.map` `f` `CategoryTheory.LocalizerMorphism.LeftResolution.w`	—	—
`comm_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.LocalizerMorphism.functor` `CategoryTheory.LocalizerMorphism.LeftResolution.X₁` `CategoryTheory.Functor.map` `f` `CategoryTheory.LocalizerMorphism.LeftResolution.w`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `comm`
`comp_f` 📖	mathematical	—	`f` `comp` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.LocalizerMorphism.LeftResolution.X₁`	—	—
`ext` 📖	—	`f`	—	—	—
`ext_iff` 📖	mathematical	—	`f`	—	`ext`
`id_f` 📖	mathematical	—	`f` `id` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.LocalizerMorphism.LeftResolution.X₁`	—	—

CategoryTheory.LocalizerMorphism.RightResolution

Definitions

Name	Category	Theorems
`X₁` 📖	CompOp	18 math math: `CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.Constructor.fromRightResolution_map`, `comp_f_assoc`, `op_X₁`, `CategoryTheory.LocalizerMorphism.LeftResolution.unop_X₁`, `unop_X₁`, `Hom.id_f`, `id_f`, `comp_f`, `Hom.comm`, `HomotopicalAlgebra.FibrantObject.instWeakEquivalenceWWeakEquivalences`, `hw`, `Hom.comp_f`, `unop_w`, `unopFunctor_map_f`, `CategoryTheory.LocalizerMorphism.LeftResolution.op_X₁`, `op_w`, `CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.Constructor.fromRightResolution_obj`, `Hom.comm_assoc`
`instCategory` 📖	CompOp	15 math math: `CategoryTheory.LocalizerMorphism.LeftResolution.opFunctor_map_f`, `CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.Constructor.fromRightResolution_map`, `comp_f_assoc`, `CategoryTheory.LocalizerMorphism.LeftResolution.opEquivalence_unitIso`, `CategoryTheory.LocalizerMorphism.LeftResolution.opEquivalence_inverse`, `CategoryTheory.LocalizerMorphism.LeftResolution.opFunctor_obj`, `HomotopicalAlgebra.FibrantObject.instIsConnectedRightResolutionWeakEquivalencesLocalizerMorphism`, `id_f`, `unopFunctor_obj`, `comp_f`, `CategoryTheory.LocalizerMorphism.isConnected_rightResolution_of_functorial_resolutions`, `unopFunctor_map_f`, `CategoryTheory.LocalizerMorphism.LeftResolution.opEquivalence_counitIso`, `CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.Constructor.fromRightResolution_obj`, `CategoryTheory.LocalizerMorphism.LeftResolution.opEquivalence_functor`
`op` 📖	CompOp	2 math math: `op_X₁`, `op_w`
`unop` 📖	CompOp	4 math math: `unop_X₁`, `unopFunctor_obj`, `unop_w`, `unopFunctor_map_f`
`unopFunctor` 📖	CompOp	4 math math: `CategoryTheory.LocalizerMorphism.LeftResolution.opEquivalence_inverse`, `unopFunctor_obj`, `unopFunctor_map_f`, `CategoryTheory.LocalizerMorphism.LeftResolution.opEquivalence_counitIso`
`w` 📖	CompOp	10 math math: `CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.Constructor.fromRightResolution_map`, `CategoryTheory.LocalizerMorphism.LeftResolution.unop_w`, `Hom.comm`, `HomotopicalAlgebra.FibrantObject.instWeakEquivalenceWWeakEquivalences`, `hw`, `unop_w`, `CategoryTheory.LocalizerMorphism.LeftResolution.op_w`, `op_w`, `CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.Constructor.fromRightResolution_obj`, `Hom.comm_assoc`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_f` 📖	mathematical	—	`Hom.f` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.LocalizerMorphism.RightResolution` `CategoryTheory.Category.toCategoryStruct` `instCategory` `X₁`	—	—
`comp_f_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `X₁` `Hom.f` `CategoryTheory.LocalizerMorphism.RightResolution` `instCategory`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `comp_f`
`hom_ext` 📖	—	`Hom.f`	—	—	`Hom.ext`
`hom_ext_iff` 📖	mathematical	—	`Hom.f`	—	`hom_ext`
`hw` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.LocalizerMorphism.functor` `X₁` `w`	—	—
`id_f` 📖	mathematical	—	`Hom.f` `CategoryTheory.CategoryStruct.id` `CategoryTheory.LocalizerMorphism.RightResolution` `CategoryTheory.Category.toCategoryStruct` `instCategory` `X₁`	—	—
`mk_surjective` 📖	—	—	—	—	`hw`
`op_X₁` 📖	mathematical	—	`CategoryTheory.LocalizerMorphism.LeftResolution.X₁` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.MorphismProperty.op` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.LocalizerMorphism.op` `Opposite.op` `op` `X₁`	—	—
`op_w` 📖	mathematical	—	`CategoryTheory.LocalizerMorphism.LeftResolution.w` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.MorphismProperty.op` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.LocalizerMorphism.op` `Opposite.op` `op` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Functor.obj` `CategoryTheory.LocalizerMorphism.functor` `X₁` `w`	—	—
`unopFunctor_map_f` 📖	mathematical	—	`CategoryTheory.LocalizerMorphism.LeftResolution.Hom.f` `Opposite.unop` `unop` `CategoryTheory.LocalizerMorphism.RightResolution` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.MorphismProperty.op` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.LocalizerMorphism.op` `CategoryTheory.Functor.map` `instCategory` `CategoryTheory.LocalizerMorphism.LeftResolution` `CategoryTheory.LocalizerMorphism.LeftResolution.instCategory` `unopFunctor` `Quiver.Hom.unop` `CategoryTheory.CategoryStruct.toQuiver` `X₁` `Hom.f`	—	—
`unopFunctor_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.LocalizerMorphism.RightResolution` `CategoryTheory.Category.opposite` `CategoryTheory.MorphismProperty.op` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.LocalizerMorphism.op` `instCategory` `CategoryTheory.LocalizerMorphism.LeftResolution` `Opposite.unop` `CategoryTheory.LocalizerMorphism.LeftResolution.instCategory` `unopFunctor` `unop`	—	—
`unop_X₁` 📖	mathematical	—	`CategoryTheory.LocalizerMorphism.LeftResolution.X₁` `Opposite.unop` `unop` `X₁` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.MorphismProperty.op` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.LocalizerMorphism.op`	—	—
`unop_w` 📖	mathematical	—	`CategoryTheory.LocalizerMorphism.LeftResolution.w` `Opposite.unop` `unop` `Quiver.Hom.unop` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.LocalizerMorphism.functor` `CategoryTheory.MorphismProperty.op` `CategoryTheory.LocalizerMorphism.op` `X₁` `w`	—	—

CategoryTheory.LocalizerMorphism.RightResolution.Hom

Definitions

Name	Category	Theorems
`comp` 📖	CompOp	1 math math: `comp_f`
`f` 📖	CompOp	12 math math: `CategoryTheory.LocalizerMorphism.LeftResolution.opFunctor_map_f`, `CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.Constructor.fromRightResolution_map`, `CategoryTheory.LocalizerMorphism.RightResolution.comp_f_assoc`, `id_f`, `ext_iff`, `CategoryTheory.LocalizerMorphism.RightResolution.id_f`, `CategoryTheory.LocalizerMorphism.RightResolution.comp_f`, `CategoryTheory.LocalizerMorphism.RightResolution.hom_ext_iff`, `comm`, `comp_f`, `CategoryTheory.LocalizerMorphism.RightResolution.unopFunctor_map_f`, `comm_assoc`
`id` 📖	CompOp	1 math math: `id_f`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comm` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.LocalizerMorphism.functor` `CategoryTheory.LocalizerMorphism.RightResolution.X₁` `CategoryTheory.LocalizerMorphism.RightResolution.w` `CategoryTheory.Functor.map` `f`	—	—
`comm_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.LocalizerMorphism.functor` `CategoryTheory.LocalizerMorphism.RightResolution.X₁` `CategoryTheory.LocalizerMorphism.RightResolution.w` `CategoryTheory.Functor.map` `f`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `comm`
`comp_f` 📖	mathematical	—	`f` `comp` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.LocalizerMorphism.RightResolution.X₁`	—	—
`ext` 📖	—	`f`	—	—	—
`ext_iff` 📖	mathematical	—	`f`	—	`ext`
`id_f` 📖	mathematical	—	`f` `id` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.LocalizerMorphism.RightResolution.X₁`	—	—

---

← Back to Index