OfAdjunction

📁 Source: Mathlib/CategoryTheory/Localization/CalculusOfFractions/OfAdjunction.lean

Statistics

Metric	Count
Definitions	0
Theorems functorCategory_inverseImage_isomorphisms_counit, functorCategory_inverseImage_isomorphisms_unit, hasLeftCalculusOfFractions, hasLeftCalculusOfFractions', hasRightCalculusOfFractions, hasRightCalculusOfFractions', isLocalization_leftAdjoint, isLocalization_leftAdjoint', isLocalization_rightAdjoint, isLocalization_rightAdjoint'	10
Total	10

CategoryTheory.Adjunction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
functorCategory_inverseImage_isomorphisms_counit 📖	mathematical	—	CategoryTheory.MorphismProperty.functorCategory CategoryTheory.MorphismProperty.inverseImage CategoryTheory.MorphismProperty.isomorphisms CategoryTheory.Functor.comp CategoryTheory.Functor.id counit	—	instIsIsoMapAppCounitOfFaithfulOfFull
functorCategory_inverseImage_isomorphisms_unit 📖	mathematical	—	CategoryTheory.MorphismProperty.functorCategory CategoryTheory.MorphismProperty.inverseImage CategoryTheory.MorphismProperty.isomorphisms CategoryTheory.Functor.id CategoryTheory.Functor.comp unit	—	instIsIsoMapAppUnitOfFaithfulOfFull
hasLeftCalculusOfFractions 📖	mathematical	CategoryTheory.MorphismProperty.IsInvertedBy CategoryTheory.MorphismProperty.functorCategory CategoryTheory.Functor.id CategoryTheory.Functor.comp unit	CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions	—	CategoryTheory.MorphismProperty.RightFraction.cases CategoryTheory.NatTrans.naturality CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.Functor.map_isIso CategoryTheory.Functor.map_inv CategoryTheory.IsIso.hom_inv_id_assoc unit_naturality CategoryTheory.cancel_epi CategoryTheory.IsSplitEpi.epi CategoryTheory.IsSplitEpi.of_iso CategoryTheory.Functor.map_comp
hasLeftCalculusOfFractions' 📖	mathematical	—	CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions CategoryTheory.MorphismProperty.inverseImage CategoryTheory.MorphismProperty.isomorphisms	—	hasLeftCalculusOfFractions CategoryTheory.MorphismProperty.IsMultiplicative.instInverseImage CategoryTheory.MorphismProperty.IsMultiplicative.instIsomorphisms functorCategory_inverseImage_isomorphisms_unit
hasRightCalculusOfFractions 📖	mathematical	CategoryTheory.MorphismProperty.IsInvertedBy CategoryTheory.MorphismProperty.functorCategory CategoryTheory.Functor.comp CategoryTheory.Functor.id counit	CategoryTheory.MorphismProperty.HasRightCalculusOfFractions	—	hasLeftCalculusOfFractions CategoryTheory.MorphismProperty.IsMultiplicative.op CategoryTheory.MorphismProperty.IsInvertedBy.op CategoryTheory.MorphismProperty.instHasRightCalculusOfFractionsUnopOfHasLeftCalculusOfFractionsOpposite
hasRightCalculusOfFractions' 📖	mathematical	—	CategoryTheory.MorphismProperty.HasRightCalculusOfFractions CategoryTheory.MorphismProperty.inverseImage CategoryTheory.MorphismProperty.isomorphisms	—	hasRightCalculusOfFractions CategoryTheory.MorphismProperty.IsMultiplicative.instInverseImage CategoryTheory.MorphismProperty.IsMultiplicative.instIsomorphisms functorCategory_inverseImage_isomorphisms_counit
isLocalization_leftAdjoint 📖	mathematical	CategoryTheory.MorphismProperty.IsInvertedBy CategoryTheory.MorphismProperty.functorCategory CategoryTheory.Functor.id CategoryTheory.Functor.comp unit	CategoryTheory.Functor.IsLocalization	—	CategoryTheory.Functor.q_isLocalization CategoryTheory.NatTrans.isIso_iff_isIso_app CategoryTheory.Localization.inverts CategoryTheory.Functor.IsLocalization.of_equivalence_target counit_isIso_of_R_fully_faithful
isLocalization_leftAdjoint' 📖	mathematical	—	CategoryTheory.Functor.IsLocalization CategoryTheory.MorphismProperty.inverseImage CategoryTheory.MorphismProperty.isomorphisms	—	isLocalization_leftAdjoint functorCategory_inverseImage_isomorphisms_unit
isLocalization_rightAdjoint 📖	mathematical	CategoryTheory.MorphismProperty.IsInvertedBy CategoryTheory.MorphismProperty.functorCategory CategoryTheory.Functor.comp CategoryTheory.Functor.id counit	CategoryTheory.Functor.IsLocalization	—	isLocalization_leftAdjoint CategoryTheory.Functor.instFullOppositeOp CategoryTheory.Functor.instFaithfulOppositeOp CategoryTheory.MorphismProperty.IsInvertedBy.op
isLocalization_rightAdjoint' 📖	mathematical	—	CategoryTheory.Functor.IsLocalization CategoryTheory.MorphismProperty.inverseImage CategoryTheory.MorphismProperty.isomorphisms	—	isLocalization_rightAdjoint functorCategory_inverseImage_isomorphisms_counit

---

← Back to Index