Commit 2022-10-12 10:35 032f11f8

View on Github →

feat(category_theory/localization): developing the predicate is_localization (#16890) When L : C ⥤ D and W : morphism_property C, a constructor for the predicate L.is_localization W is introduced: it takes as inputs the universal property of the localized category. In this PR, it is also shown that is L.is_localization W, the functor L is essentially surjective.

Estimated changes

Modified src/category_theory/localization/predicate.lean

added theorem category_theory.functor.is_localization.for_id

added theorem category_theory.functor.is_localization.mk'

added def category_theory.localization.Q_comp_equivalence_from_model_functor_iso

added def category_theory.localization.comp_equivalence_from_model_inverse_iso

added def category_theory.localization.equivalence_from_model

added theorem category_theory.localization.ess_surj

added theorem category_theory.localization.inverts

added def category_theory.localization.iso_of_hom

added structure category_theory.localization.strict_universal_property_fixed_target

added def category_theory.localization.strict_universal_property_fixed_target_Q

added def category_theory.localization.strict_universal_property_fixed_target_id

Modified src/category_theory/whiskering.lean

added theorem category_theory.functor.assoc