Commit 2023-03-27 13:48 363572d1

View on Github →

feat: port CategoryTheory.Localization.Predicate (#2930)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Localization/Predicate.lean

added theorem CategoryTheory.Functor.IsLocalization.for_id

added theorem CategoryTheory.Functor.IsLocalization.mk'

added theorem CategoryTheory.Functor.IsLocalization.of_equivalence_target

added theorem CategoryTheory.Functor.IsLocalization.of_iso

added def CategoryTheory.Localization.Lifting.iso

added def CategoryTheory.Localization.Lifting.ofIsos

added structure CategoryTheory.Localization.StrictUniversalPropertyFixedTarget

added def CategoryTheory.Localization.compEquivalenceFromModelInverseIso

added theorem CategoryTheory.Localization.comp_liftNatTrans

added def CategoryTheory.Localization.equivalenceFromModel

added theorem CategoryTheory.Localization.essSurj

added def CategoryTheory.Localization.fac

added def CategoryTheory.Localization.functorEquivalence

added theorem CategoryTheory.Localization.inverts

added def CategoryTheory.Localization.isoOfHom

added def CategoryTheory.Localization.lift

added def CategoryTheory.Localization.liftNatIso

added def CategoryTheory.Localization.liftNatTrans

added theorem CategoryTheory.Localization.liftNatTrans_app

added theorem CategoryTheory.Localization.liftNatTrans_id

added theorem CategoryTheory.Localization.natTrans_ext

added def CategoryTheory.Localization.qCompEquivalenceFromModelFunctorIso

added def CategoryTheory.Localization.strictUniversalPropertyFixedTargetId

added def CategoryTheory.Localization.strictUniversalPropertyFixedTargetQ

added def CategoryTheory.Localization.whiskeringLeftFunctor'

added theorem CategoryTheory.Localization.whiskeringLeftFunctor'_eq

added theorem CategoryTheory.Localization.whiskeringLeftFunctor'_obj

added def CategoryTheory.Localization.whiskeringLeftFunctor