Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-28 01:01 350a3817

View on Github →

feat(category_theory): construction of the localized category (#14422) When W : morphism_property C is a class of morphisms in a category C, this PR constructs the localized category localization W obtained by adding formal inverses to the morphisms in W.

Estimated changes

Modified docs/references.bib

Modified src/category_theory/arrow.lean

added theorem category_theory.arrow.mk_eq

Modified src/category_theory/category/Quiv.lean

modified def category_theory.Quiv.lift

Modified src/category_theory/eq_to_hom.lean

added theorem category_theory.functor.congr_inv_of_congr_hom

Created src/category_theory/localization/construction.lean

added def category_theory.localization.construction.Wiso

added theorem category_theory.localization.construction.fac

added def category_theory.localization.construction.lift

added def category_theory.localization.construction.lift_to_path_category

added structure category_theory.localization.construction.loc_quiver

added inductive category_theory.localization.construction.relations

added theorem category_theory.localization.construction.uniq

added def category_theory.localization.construction.ι_paths

added def category_theory.localization.construction.ψ₁

added def category_theory.localization.construction.ψ₂

added def category_theory.morphism_property.Q

added def category_theory.morphism_property.localization

Modified src/category_theory/morphism_property.lean

added def category_theory.morphism_property.is_inverted_by

Modified src/combinatorics/quiver/path.lean

added theorem prefunctor.map_path_to_path