Commit 2022-09-30 13:10 a52be2a5

View on Github →

feat(category_theory/localization): whiskering_left_equivalence and definition of the predicate (#16646) In this PR, an equivalence localization.construction.whiskering_left_equivalence W D : (W.localization ⥤ D) ≌ W.functors_inverting D is obtained and the predicate L.is_localization W is defined for a functor L : C ⥤ D.

Estimated changes

Modified src/category_theory/localization/construction.lean

added theorem category_theory.localization.construction.nat_trans_hcomp_injective

added def category_theory.localization.construction.whiskering_left_equivalence.counit_iso

added def category_theory.localization.construction.whiskering_left_equivalence.functor

added def category_theory.localization.construction.whiskering_left_equivalence.inverse

added def category_theory.localization.construction.whiskering_left_equivalence.unit_iso

added def category_theory.localization.construction.whiskering_left_equivalence

added theorem category_theory.morphism_property.Q_inverts

Created src/category_theory/localization/predicate.lean

Modified src/category_theory/morphism_property.lean

added def category_theory.morphism_property.functors_inverting.mk

added def category_theory.morphism_property.functors_inverting

added theorem category_theory.morphism_property.is_inverted_by.of_comp