IsInvertedBy

📁 Source: Mathlib/CategoryTheory/MorphismProperty/IsInvertedBy.lean

Statistics

Metric	Count
Definitions FunctorsInverting, mk, IsInvertedBy, instCategoryFunctorsInverting	4
Theorems comp_hom, comp_hom_assoc, ext, ext_iff, hom_ext, hom_ext_iff, id_hom, iff_comp, iff_le_inverseImage_isomorphisms, iff_map_le_isomorphisms, iff_of_iso, isoClosure_iff, leftOp, map_iff, of_comp, of_le, op, pi, prod, rightOp, unop	21
Total	25

CategoryTheory.MorphismProperty

Definitions

Name	Category	Theorems
FunctorsInverting 📖	CompOp	15 math math: CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.functor_obj_obj_map, FunctorsInverting.id_hom, CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.functor_obj_obj_obj, CategoryTheory.Localization.whiskeringLeftFunctor'_eq, CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.inverse_map_app, CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.functor_map_hom_app, FunctorsInverting.comp_hom_assoc, CategoryTheory.Localization.instIsEquivalenceFunctorFunctorsInvertingWhiskeringLeftFunctor, CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.inverse_obj_map, CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.inverse_obj_obj, CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.unitIso_inv, FunctorsInverting.comp_hom, CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.counitIso_inv, CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.unitIso_hom, CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.counitIso_hom
IsInvertedBy 📖	MathDef	37 math math: IsInvertedBy.iff_comp, CategoryTheory.ObjectProperty.isoModSerre_isInvertedBy_iff, HomotopicalAlgebra.BifibrantObject.inverts_iff_factors, CategoryTheory.Functor.IsLocalization.inverts, IsCompatibleWithShift.shiftFunctor_comp_inverts, CategoryTheory.ObjectProperty.inverseImage_trW_isInverted, IsInvertedBy.iff_map_le_isomorphisms, HomotopyCategory.quotient_inverts_homotopyEquivalences, LeftFraction.Localization.StrictUniversalPropertyFixedTarget.inverts, HomologicalComplexUpToQuasiIso.Q_inverts_homotopyEquivalences, CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.inverts, CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.functor_obj_obj_map, FunctorsInverting.id_hom, CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.functor_obj_obj_obj, CategoryTheory.GrothendieckTopology.W_isInvertedBy_whiskeringRight_presheafToSheaf, IsInvertedBy.iff_of_iso, CategoryTheory.Functor.mapHomologicalComplex_upToQuasiIso_Q_inverts_quasiIso, CategoryTheory.Localization.whiskeringLeftFunctor'_eq, CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.inverse_map_app, CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.functor_map_hom_app, CategoryTheory.GrothendieckTopology.Point.W_isInvertedBy_presheafFiber, FunctorsInverting.comp_hom_assoc, CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.inverse_obj_map, IsInvertedBy.isoClosure_iff, HomologicalComplexUpToQuasiIso.Qh_inverts_quasiIso, IsInvertedBy.iff_le_inverseImage_isomorphisms, FunctorsInverting.ext_iff, CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.inverse_obj_obj, CategoryTheory.Localization.HasProductsOfShapeAux.inverts, FunctorsInverting.comp_hom, CategoryTheory.LocalizerMorphism.inverts, CategoryTheory.Localization.inverts, Q_inverts, HomotopyCategory.homologyFunctor_inverts_quasiIso, HomologicalComplex.homologyFunctor_inverts_quasiIso, IsInvertedBy.map_iff, FunctorsInverting.hom_ext_iff
instCategoryFunctorsInverting 📖	CompOp	15 math math: CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.functor_obj_obj_map, FunctorsInverting.id_hom, CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.functor_obj_obj_obj, CategoryTheory.Localization.whiskeringLeftFunctor'_eq, CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.inverse_map_app, CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.functor_map_hom_app, FunctorsInverting.comp_hom_assoc, CategoryTheory.Localization.instIsEquivalenceFunctorFunctorsInvertingWhiskeringLeftFunctor, CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.inverse_obj_map, CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.inverse_obj_obj, CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.unitIso_inv, FunctorsInverting.comp_hom, CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.counitIso_inv, CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.unitIso_hom, CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.counitIso_hom

CategoryTheory.MorphismProperty.FunctorsInverting

Definitions

Name	Category	Theorems
mk 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_hom 📖	mathematical	—	CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.MorphismProperty.IsInvertedBy CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.CategoryStruct.comp CategoryTheory.MorphismProperty.FunctorsInverting CategoryTheory.Category.toCategoryStruct CategoryTheory.MorphismProperty.instCategoryFunctorsInverting	—	—
comp_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.MorphismProperty.IsInvertedBy CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.MorphismProperty.FunctorsInverting CategoryTheory.MorphismProperty.instCategoryFunctorsInverting	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_hom
ext 📖	—	CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.MorphismProperty.IsInvertedBy	—	—	—
ext_iff 📖	mathematical	—	CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.MorphismProperty.IsInvertedBy	—	ext
hom_ext 📖	—	CategoryTheory.NatTrans.app CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.MorphismProperty.IsInvertedBy CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory	—	—	CategoryTheory.ObjectProperty.hom_ext CategoryTheory.NatTrans.ext
hom_ext_iff 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.MorphismProperty.IsInvertedBy CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory	—	hom_ext
id_hom 📖	mathematical	—	CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.MorphismProperty.IsInvertedBy CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.CategoryStruct.id CategoryTheory.MorphismProperty.FunctorsInverting CategoryTheory.Category.toCategoryStruct CategoryTheory.MorphismProperty.instCategoryFunctorsInverting	—	—

CategoryTheory.MorphismProperty.IsInvertedBy

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iff_comp 📖	mathematical	—	CategoryTheory.MorphismProperty.IsInvertedBy CategoryTheory.Functor.comp	—	CategoryTheory.isIso_of_reflects_iso of_comp
iff_le_inverseImage_isomorphisms 📖	mathematical	—	CategoryTheory.MorphismProperty.IsInvertedBy CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.MorphismProperty.inverseImage CategoryTheory.MorphismProperty.isomorphisms	—	—
iff_map_le_isomorphisms 📖	mathematical	—	CategoryTheory.MorphismProperty.IsInvertedBy CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.MorphismProperty.map CategoryTheory.MorphismProperty.isomorphisms	—	iff_le_inverseImage_isomorphisms CategoryTheory.MorphismProperty.map_le_iff CategoryTheory.MorphismProperty.RespectsIso.isomorphisms
iff_of_iso 📖	mathematical	—	CategoryTheory.MorphismProperty.IsInvertedBy	—	CategoryTheory.NatIso.isIso_map_iff
isoClosure_iff 📖	mathematical	—	CategoryTheory.MorphismProperty.IsInvertedBy CategoryTheory.MorphismProperty.isoClosure	—	CategoryTheory.MorphismProperty.le_isoClosure CategoryTheory.Arrow.iso_w' CategoryTheory.Functor.map_comp CategoryTheory.IsIso.comp_isIso CategoryTheory.Functor.map_isIso CategoryTheory.Arrow.isIso_left CategoryTheory.Iso.isIso_inv CategoryTheory.Arrow.isIso_right CategoryTheory.Iso.isIso_hom
leftOp 📖	mathematical	CategoryTheory.MorphismProperty.IsInvertedBy Opposite CategoryTheory.Category.opposite	CategoryTheory.MorphismProperty.op CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.leftOp	—	CategoryTheory.isIso_unop
map_iff 📖	mathematical	—	CategoryTheory.MorphismProperty.IsInvertedBy CategoryTheory.MorphismProperty.map CategoryTheory.Functor.comp	—	CategoryTheory.MorphismProperty.map_map
of_comp 📖	mathematical	CategoryTheory.MorphismProperty.IsInvertedBy	CategoryTheory.Functor.comp	—	CategoryTheory.Functor.map_isIso
of_le 📖	—	CategoryTheory.MorphismProperty.IsInvertedBy CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra	—	—	—
op 📖	mathematical	CategoryTheory.MorphismProperty.IsInvertedBy	Opposite CategoryTheory.Category.opposite CategoryTheory.MorphismProperty.op CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.op	—	CategoryTheory.isIso_op
pi 📖	mathematical	CategoryTheory.MorphismProperty.IsInvertedBy	CategoryTheory.pi CategoryTheory.MorphismProperty.pi CategoryTheory.Functor.pi	—	CategoryTheory.isIso_pi_iff
prod 📖	mathematical	CategoryTheory.MorphismProperty.IsInvertedBy	CategoryTheory.prod' CategoryTheory.MorphismProperty.prod CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.prod	—	CategoryTheory.isIso_prod_iff
rightOp 📖	mathematical	CategoryTheory.MorphismProperty.IsInvertedBy Opposite CategoryTheory.Category.opposite CategoryTheory.MorphismProperty.op CategoryTheory.Category.toCategoryStruct	CategoryTheory.Functor.rightOp	—	CategoryTheory.isIso_op
unop 📖	mathematical	CategoryTheory.MorphismProperty.IsInvertedBy Opposite CategoryTheory.Category.opposite CategoryTheory.MorphismProperty.op CategoryTheory.Category.toCategoryStruct	CategoryTheory.Functor.unop	—	CategoryTheory.isIso_unop

---

← Back to Index