Predicate

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

Statistics

Metric	Count
Definitions AreEqualizedByLocalization, compLeft, compRight, id, iso, iso', ofIsos, StrictUniversalPropertyFixedTarget, compEquivalenceFromModelInverseIso, compUniqFunctor, compUniqInverse, equivalenceFromModel, fac, functorEquivalence, groupoid, instInhabitedStrictUniversalPropertyFixedTargetLocalizationQ, instLiftingFunctorUniq, instLiftingInverseUniq, isoOfHom, isoUniqFunctor, liftNatIso, liftNatTrans, liftingConstructionLift, liftingLift, qCompEquivalenceFromModelFunctorIso, strictUniversalPropertyFixedTargetId, strictUniversalPropertyFixedTargetQ, uniq, whiskeringLeftFunctor, whiskeringLeftFunctor'	30
Theorems map_eq, map_eq_of_isInvertedBy, mk, for_id, instCompOfIsEquivalence, inverts, isEquivalence, mk', of_equivalence_target, of_isEquivalence, of_iso, q_isLocalization, wInv_eq_isoOfHom_inv, wIso_eq_isoOfHom, compLeft_iso, compRight_iso, id_iso, ofIsos_iso, fac, inverts, uniq, comp_liftNatTrans, comp_liftNatTrans_assoc, essSurj, faithful_whiskeringLeft, full_whiskeringLeft, instFaithfulFunctorWhiskeringLeftFunctor', instFullFunctorWhiskeringLeftFunctor', instIsEquivalenceFunctorFunctorsInvertingWhiskeringLeftFunctor, instIsEquivalenceLocalizationLift, instIsGroupoidLocalizationTopMorphismProperty, inverts, isGroupoid, isoOfHom_hom, isoOfHom_hom_inv_id, isoOfHom_hom_inv_id_assoc, isoOfHom_id_inv, isoOfHom_inv_hom_id, isoOfHom_inv_hom_id_assoc, liftNatIso_hom, liftNatIso_inv, liftNatTrans_app, liftNatTrans_id, morphismProperty_eq_top, natTrans_ext, strictUniversalPropertyFixedTargetId_lift, strictUniversalPropertyFixedTargetQ_lift, uniq_symm, whiskeringLeftFunctor'_eq, whiskeringLeftFunctor'_obj, areEqualizedByLocalization_iff	51
Total	81

CategoryTheory

Definitions

Name	Category	Theorems
AreEqualizedByLocalization 📖	MathDef	3 math math: areEqualizedByLocalization_iff, ComplexShape.QFactorsThroughHomotopy.areEqualizedByLocalization, AreEqualizedByLocalization.mk

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
areEqualizedByLocalization_iff 📖	mathematical	—	AreEqualizedByLocalization Functor.map	—	Functor.q_isLocalization NatIso.naturality_1

CategoryTheory.AreEqualizedByLocalization

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_eq 📖	mathematical	CategoryTheory.AreEqualizedByLocalization	CategoryTheory.Functor.map	—	CategoryTheory.areEqualizedByLocalization_iff
map_eq_of_isInvertedBy 📖	mathematical	CategoryTheory.AreEqualizedByLocalization CategoryTheory.MorphismProperty.IsInvertedBy	CategoryTheory.Functor.map	—	CategoryTheory.Functor.q_isLocalization CategoryTheory.NatIso.naturality_1 map_eq
mk 📖	mathematical	CategoryTheory.Functor.map	CategoryTheory.AreEqualizedByLocalization	—	CategoryTheory.areEqualizedByLocalization_iff

CategoryTheory.Functor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
q_isLocalization 📖	mathematical	—	IsLocalization CategoryTheory.MorphismProperty.Localization CategoryTheory.MorphismProperty.instCategoryLocalization CategoryTheory.MorphismProperty.Q	—	CategoryTheory.MorphismProperty.Q_inverts CategoryTheory.Localization.Construction.uniq CategoryTheory.Localization.Construction.fac isEquivalence_refl

CategoryTheory.Functor.IsLocalization

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
for_id 📖	mathematical	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.MorphismProperty.isomorphisms	CategoryTheory.Functor.IsLocalization CategoryTheory.Functor.id	—	mk'
instCompOfIsEquivalence 📖	mathematical	—	CategoryTheory.Functor.IsLocalization CategoryTheory.Functor.comp	—	of_equivalence_target
inverts 📖	mathematical	—	CategoryTheory.MorphismProperty.IsInvertedBy	—	—
isEquivalence 📖	mathematical	—	CategoryTheory.Functor.IsEquivalence CategoryTheory.MorphismProperty.Localization CategoryTheory.MorphismProperty.instCategoryLocalization CategoryTheory.Localization.Construction.lift inverts	—	—
mk' 📖	mathematical	—	CategoryTheory.Functor.IsLocalization	—	CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.inverts CategoryTheory.Functor.IsEquivalence.mk' CategoryTheory.MorphismProperty.Q_inverts CategoryTheory.Localization.Construction.uniq CategoryTheory.Localization.Construction.fac CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.fac CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.uniq
of_equivalence_target 📖	mathematical	—	CategoryTheory.Functor.IsLocalization	—	CategoryTheory.MorphismProperty.IsInvertedBy.iff_of_iso CategoryTheory.MorphismProperty.IsInvertedBy.of_comp CategoryTheory.Localization.inverts CategoryTheory.Functor.q_isLocalization CategoryTheory.Functor.isEquivalence_of_iso CategoryTheory.Functor.isEquivalence_trans CategoryTheory.Localization.instIsEquivalenceLocalizationLift CategoryTheory.Equivalence.isEquivalence_functor
of_isEquivalence 📖	mathematical	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.MorphismProperty.isomorphisms	CategoryTheory.Functor.IsLocalization	—	of_equivalence_target for_id
of_iso 📖	mathematical	—	CategoryTheory.Functor.IsLocalization	—	CategoryTheory.Localization.inverts CategoryTheory.MorphismProperty.IsInvertedBy.iff_of_iso CategoryTheory.Functor.isEquivalence_of_iso CategoryTheory.Functor.q_isLocalization CategoryTheory.Localization.instIsEquivalenceLocalizationLift

CategoryTheory.Localization

Definitions

Name	Category	Theorems
StrictUniversalPropertyFixedTarget 📖	CompData	—
compEquivalenceFromModelInverseIso 📖	CompOp	—
compUniqFunctor 📖	CompOp	1 math math: CategoryTheory.MorphismProperty.LeftFraction.map_compatibility
compUniqInverse 📖	CompOp	—
equivalenceFromModel 📖	CompOp	—
fac 📖	CompOp	2 math math: CategoryTheory.Functor.instIsRightDerivedFunctorLiftInvFac, CategoryTheory.Functor.instIsLeftDerivedFunctorLiftHomFac
functorEquivalence 📖	CompOp	—
groupoid 📖	CompOp	—
instInhabitedStrictUniversalPropertyFixedTargetLocalizationQ 📖	CompOp	—
instLiftingFunctorUniq 📖	CompOp	—
instLiftingInverseUniq 📖	CompOp	—
isoOfHom 📖	CompOp	16 math math: CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.Constructor.fromRightResolution_map, isoOfHom_unop, isoOfHom_inv_hom_id, Construction.wInv_eq_isoOfHom_inv, isoOfHom_op_inv, SmallHom.equiv_mkInv, isoOfHom_hom, isoOfHom_hom_inv_id, isoOfHom_hom_inv_id_assoc, SmallShiftedHom.equiv_mk₀Inv, isoOfHom_inv_hom_id_assoc, CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.Constructor.fromRightResolution_obj, homEquiv_isoOfHom_inv, Construction.wIso_eq_isoOfHom, CategoryTheory.MorphismProperty.LeftFraction.map_eq, isoOfHom_id_inv
isoUniqFunctor 📖	CompOp	—
liftNatIso 📖	CompOp	2 math math: liftNatIso_inv, liftNatIso_hom
liftNatTrans 📖	CompOp	8 math math: liftNatTrans_add, liftNatTrans_zero, comp_liftNatTrans, liftNatIso_inv, liftNatTrans_app, comp_liftNatTrans_assoc, liftNatTrans_id, liftNatIso_hom
liftingConstructionLift 📖	CompOp	—
liftingLift 📖	CompOp	—
qCompEquivalenceFromModelFunctorIso 📖	CompOp	—
strictUniversalPropertyFixedTargetId 📖	CompOp	1 math math: strictUniversalPropertyFixedTargetId_lift
strictUniversalPropertyFixedTargetQ 📖	CompOp	1 math math: strictUniversalPropertyFixedTargetQ_lift
uniq 📖	CompOp	2 math math: CategoryTheory.MorphismProperty.LeftFraction.map_compatibility, uniq_symm
whiskeringLeftFunctor 📖	CompOp	2 math math: whiskeringLeftFunctor'_eq, instIsEquivalenceFunctorFunctorsInvertingWhiskeringLeftFunctor
whiskeringLeftFunctor' 📖	CompOp	4 math math: instFullFunctorWhiskeringLeftFunctor', instFaithfulFunctorWhiskeringLeftFunctor', whiskeringLeftFunctor'_eq, whiskeringLeftFunctor'_obj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_liftNatTrans 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category liftNatTrans	—	natTrans_ext liftNatTrans_app CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_app_assoc
comp_liftNatTrans_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category liftNatTrans	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_liftNatTrans
essSurj 📖	mathematical	—	CategoryTheory.Functor.EssSurj	—	—
faithful_whiskeringLeft 📖	mathematical	—	CategoryTheory.Functor.Faithful CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft	—	instFaithfulFunctorWhiskeringLeftFunctor'
full_whiskeringLeft 📖	mathematical	—	CategoryTheory.Functor.Full CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft	—	instFullFunctorWhiskeringLeftFunctor'
instFaithfulFunctorWhiskeringLeftFunctor' 📖	mathematical	—	CategoryTheory.Functor.Faithful CategoryTheory.Functor CategoryTheory.Functor.category whiskeringLeftFunctor'	—	whiskeringLeftFunctor'_eq CategoryTheory.Functor.Faithful.comp CategoryTheory.Functor.IsEquivalence.faithful instIsEquivalenceFunctorFunctorsInvertingWhiskeringLeftFunctor CategoryTheory.InducedCategory.faithful
instFullFunctorWhiskeringLeftFunctor' 📖	mathematical	—	CategoryTheory.Functor.Full CategoryTheory.Functor CategoryTheory.Functor.category whiskeringLeftFunctor'	—	whiskeringLeftFunctor'_eq CategoryTheory.Functor.Full.comp CategoryTheory.Functor.IsEquivalence.full instIsEquivalenceFunctorFunctorsInvertingWhiskeringLeftFunctor CategoryTheory.InducedCategory.full
instIsEquivalenceFunctorFunctorsInvertingWhiskeringLeftFunctor 📖	mathematical	—	CategoryTheory.Functor.IsEquivalence CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.MorphismProperty.FunctorsInverting CategoryTheory.MorphismProperty.instCategoryFunctorsInverting whiskeringLeftFunctor	—	CategoryTheory.MorphismProperty.FunctorsInverting.ext inverts Construction.fac CategoryTheory.MorphismProperty.FunctorsInverting.hom_ext CategoryTheory.ObjectProperty.eqToHom_hom CategoryTheory.Functor.congr_obj CategoryTheory.eqToHom_app CategoryTheory.eqToHom_refl CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.Functor.isEquivalence_of_iso CategoryTheory.Functor.isEquivalence_trans CategoryTheory.Functor.instIsEquivalenceObjWhiskeringLeft CategoryTheory.Equivalence.isEquivalence_functor
instIsEquivalenceLocalizationLift 📖	mathematical	—	CategoryTheory.Functor.IsEquivalence CategoryTheory.MorphismProperty.Localization CategoryTheory.MorphismProperty.instCategoryLocalization Construction.lift inverts	—	CategoryTheory.Functor.IsLocalization.isEquivalence
instIsGroupoidLocalizationTopMorphismProperty 📖	mathematical	—	CategoryTheory.IsGroupoid CategoryTheory.MorphismProperty.Localization Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.MorphismProperty.instCategoryLocalization	—	isGroupoid CategoryTheory.Functor.q_isLocalization
inverts 📖	mathematical	—	CategoryTheory.MorphismProperty.IsInvertedBy	—	CategoryTheory.Functor.IsLocalization.inverts
isGroupoid 📖	mathematical	—	CategoryTheory.IsGroupoid	—	CategoryTheory.isGroupoid_iff_isomorphisms_eq_top morphismProperty_eq_top CategoryTheory.MorphismProperty.RespectsIso.isomorphisms CategoryTheory.MorphismProperty.IsMultiplicative.instIsomorphisms inverts CategoryTheory.Iso.isIso_inv
isoOfHom_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Functor.obj isoOfHom CategoryTheory.Functor.map	—	—
isoOfHom_hom_inv_id 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.Iso.inv isoOfHom CategoryTheory.CategoryStruct.id	—	CategoryTheory.Iso.hom_inv_id
isoOfHom_hom_inv_id_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.Iso.inv isoOfHom	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' isoOfHom_hom_inv_id
isoOfHom_id_inv 📖	mathematical	CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	CategoryTheory.Iso.inv CategoryTheory.Functor.obj isoOfHom	—	CategoryTheory.cancel_mono CategoryTheory.IsSplitMono.mono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_hom CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.id_comp isoOfHom_hom CategoryTheory.Functor.map_id
isoOfHom_inv_hom_id 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Iso.inv isoOfHom CategoryTheory.Functor.map CategoryTheory.CategoryStruct.id	—	CategoryTheory.Iso.inv_hom_id
isoOfHom_inv_hom_id_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Iso.inv isoOfHom CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' isoOfHom_inv_hom_id
liftNatIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category liftNatIso liftNatTrans	—	—
liftNatIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category liftNatIso liftNatTrans	—	—
liftNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app liftNatTrans CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.comp CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category Lifting.iso CategoryTheory.Iso.inv	—	CategoryTheory.congr_app instFullFunctorWhiskeringLeftFunctor' CategoryTheory.Functor.map_preimage
liftNatTrans_id 📖	mathematical	—	liftNatTrans CategoryTheory.CategoryStruct.id CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category	—	natTrans_ext liftNatTrans_app CategoryTheory.Category.id_comp CategoryTheory.Iso.hom_inv_id_app
morphismProperty_eq_top 📖	mathematical	CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.Iso.inv isoOfHom	Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra	—	CategoryTheory.Functor.q_isLocalization Construction.morphismProperty_eq_top CategoryTheory.MorphismProperty.IsStableUnderComposition.inverseImage CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition CategoryTheory.MorphismProperty.arrow_mk_iso_iff Construction.wInv_eq_isoOfHom_inv CategoryTheory.cancel_mono CategoryTheory.IsSplitMono.mono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_hom CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id isoOfHom_hom CategoryTheory.NatTrans.naturality CategoryTheory.Functor.comp_map CategoryTheory.Functor.map_comp_assoc isoOfHom_inv_hom_id CategoryTheory.Functor.map_id CategoryTheory.Category.id_comp CategoryTheory.MorphismProperty.map_inverseImage_eq_of_isEquivalence CategoryTheory.Equivalence.isEquivalence_functor CategoryTheory.MorphismProperty.map_top_eq_top_of_essSurj_of_full CategoryTheory.Equivalence.essSurj_functor CategoryTheory.Equivalence.full_functor
natTrans_ext 📖	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj	—	—	CategoryTheory.NatTrans.ext' essSurj CategoryTheory.cancel_epi CategoryTheory.IsSplitEpi.epi CategoryTheory.instIsSplitEpiMap CategoryTheory.IsSplitEpi.of_iso CategoryTheory.Iso.isIso_hom CategoryTheory.NatTrans.naturality
strictUniversalPropertyFixedTargetId_lift 📖	mathematical	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.MorphismProperty.isomorphisms CategoryTheory.MorphismProperty.IsInvertedBy	StrictUniversalPropertyFixedTarget.lift CategoryTheory.Functor.id strictUniversalPropertyFixedTargetId	—	—
strictUniversalPropertyFixedTargetQ_lift 📖	mathematical	CategoryTheory.MorphismProperty.IsInvertedBy	StrictUniversalPropertyFixedTarget.lift CategoryTheory.MorphismProperty.Localization CategoryTheory.MorphismProperty.instCategoryLocalization CategoryTheory.MorphismProperty.Q strictUniversalPropertyFixedTargetQ Construction.lift	—	—
uniq_symm 📖	mathematical	—	CategoryTheory.Equivalence.symm uniq	—	CategoryTheory.Equivalence.ext CategoryTheory.Functor.isoWhiskerRight_trans CategoryTheory.Iso.trans_assoc CategoryTheory.Equivalence.mk'.congr_simp
whiskeringLeftFunctor'_eq 📖	mathematical	—	whiskeringLeftFunctor' CategoryTheory.Functor.comp CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.MorphismProperty.FunctorsInverting CategoryTheory.MorphismProperty.instCategoryFunctorsInverting whiskeringLeftFunctor CategoryTheory.inducedFunctor CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.MorphismProperty.IsInvertedBy CategoryTheory.ObjectProperty.FullSubcategory.obj	—	—
whiskeringLeftFunctor'_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category whiskeringLeftFunctor' CategoryTheory.Functor.comp	—	—

CategoryTheory.Localization.Construction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
wInv_eq_isoOfHom_inv 📖	mathematical	—	wInv CategoryTheory.Iso.inv CategoryTheory.MorphismProperty.Localization CategoryTheory.MorphismProperty.instCategoryLocalization CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Q CategoryTheory.Localization.isoOfHom CategoryTheory.Functor.q_isLocalization	—	CategoryTheory.Functor.q_isLocalization wIso_eq_isoOfHom
wIso_eq_isoOfHom 📖	mathematical	—	wIso CategoryTheory.Localization.isoOfHom CategoryTheory.MorphismProperty.Localization CategoryTheory.MorphismProperty.instCategoryLocalization CategoryTheory.MorphismProperty.Q CategoryTheory.Functor.q_isLocalization	—	CategoryTheory.Iso.ext CategoryTheory.Functor.q_isLocalization

CategoryTheory.Localization.Lifting

Definitions

Name	Category	Theorems
compLeft 📖	CompOp	1 math math: compLeft_iso
compRight 📖	CompOp	2 math math: CategoryTheory.Localization.equivalence_counitIso_app, compRight_iso
id 📖	CompOp	1 math math: id_iso
iso 📖	CompOp	27 math math: CategoryTheory.Localization.Monoidal.curriedTensorPreIsoPost_hom_app_app, compLeft_iso, CategoryTheory.Localization.Monoidal.lifting_isMonoidal, CategoryTheory.Localization.Monoidal.curriedTensorPreIsoPost_hom_app_app', ofIsos_iso, CategoryTheory.Localization.equivalence_counitIso_app, compRight_iso, CategoryTheory.Functor.commShiftOfLocalization_iso_inv_app, CategoryTheory.Functor.commShiftOfLocalization.iso_inv_app, CategoryTheory.Localization.Monoidal.functorMonoidalOfComp_μ, CategoryTheory.Localization.lift₂_iso_hom_app_app₂, CategoryTheory.Localization.Monoidal.functorMonoidalOfComp_ε, CategoryTheory.Localization.liftNatTrans_app, CategoryTheory.Functor.commShiftOfLocalization.iso_inv_app_assoc, CategoryTheory.Localization.Monoidal.functorMonoidalOfComp_ε_assoc, CategoryTheory.Localization.Monoidal.lifting₂CurriedTensorPost_iso, id_iso, CategoryTheory.Functor.commShiftOfLocalization.iso_hom_app, CategoryTheory.Localization.Monoidal.functorCoreMonoidalOfComp_εIso_inv, CategoryTheory.Localization.Monoidal.lifting₂CurriedTensorPre_iso, CategoryTheory.Functor.commShiftOfLocalization_iso_hom_app, CategoryTheory.NatTrans.commShift_iso_hom_of_localization, CategoryTheory.Functor.commShiftOfLocalization.iso_hom_app_assoc, CategoryTheory.Localization.Monoidal.curriedTensorPreIsoPost_hom_app_app_assoc, CategoryTheory.Localization.lift₂_iso_hom_app_app₁, CategoryTheory.Localization.Monoidal.functorMonoidalOfComp_μ_assoc, CategoryTheory.Localization.Monoidal.functorCoreMonoidalOfComp_εIso_hom
iso' 📖	CompOp	—
ofIsos 📖	CompOp	1 math math: ofIsos_iso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compLeft_iso 📖	mathematical	—	iso CategoryTheory.Functor.comp compLeft CategoryTheory.Iso.refl CategoryTheory.Functor CategoryTheory.Functor.category	—	—
compRight_iso 📖	mathematical	—	iso CategoryTheory.Functor.comp compRight CategoryTheory.Functor.isoWhiskerRight	—	—
id_iso 📖	mathematical	—	iso CategoryTheory.Functor.id id CategoryTheory.Functor.rightUnitor	—	—
ofIsos_iso 📖	mathematical	—	iso ofIsos CategoryTheory.Iso.trans CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.isoWhiskerLeft CategoryTheory.Iso.symm	—	—

CategoryTheory.Localization.StrictUniversalPropertyFixedTarget

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fac 📖	mathematical	CategoryTheory.MorphismProperty.IsInvertedBy	CategoryTheory.Functor.comp lift	—	—
inverts 📖	mathematical	—	CategoryTheory.MorphismProperty.IsInvertedBy	—	—
uniq 📖	—	CategoryTheory.Functor.comp	—	—	—

---

← Back to Index