Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-06 07:48 8efef279

View on Github →

feat(category_theory/localization): localization of the opposite category (#17199) If a functor L : C ⥤ D is a localization functor for W : morphism_property C, it is shown in this PR that L.op : Cᵒᵖ ⥤ Dᵒᵖ is also a localization functor.

Estimated changes

Created src/category_theory/localization/opposite.lean

added def category_theory.localization.strict_universal_property_fixed_target.op

Modified src/category_theory/localization/predicate.lean

added theorem category_theory.functor.is_localization.of_equivalence_target

added theorem category_theory.functor.is_localization.of_iso

Modified src/category_theory/morphism_property.lean

added theorem category_theory.morphism_property.is_inverted_by.iff_of_iso

added theorem category_theory.morphism_property.is_inverted_by.left_op

modified theorem category_theory.morphism_property.is_inverted_by.of_comp

added theorem category_theory.morphism_property.is_inverted_by.op

added theorem category_theory.morphism_property.is_inverted_by.right_op

added theorem category_theory.morphism_property.is_inverted_by.unop

Modified src/category_theory/natural_isomorphism.lean

added theorem category_theory.nat_iso.is_iso_map_iff

Modified src/category_theory/opposites.lean

added theorem category_theory.functor.right_op_left_op_eq