Mathlib Changelog
Changelog
About
Github
Commit
2022-08-12 04:23
fc739bf5
View on Github →
feat(category_theory/localization): extension of natural transformations (
#15747
)
Estimated changes
Modified
src/category_theory/localization/construction.lean
added
def
category_theory.localization.construction.Winv
added
theorem
category_theory.localization.construction.morphism_property_is_top'
added
theorem
category_theory.localization.construction.morphism_property_is_top
added
def
category_theory.localization.construction.nat_trans_extension.app
added
theorem
category_theory.localization.construction.nat_trans_extension.app_eq
added
def
category_theory.localization.construction.nat_trans_extension
added
theorem
category_theory.localization.construction.nat_trans_extension_hcomp
added
def
category_theory.localization.construction.obj_equiv
Modified
src/category_theory/morphism_property.lean
added
theorem
category_theory.morphism_property.naturality_property.is_stable_under_composition
added
theorem
category_theory.morphism_property.naturality_property.is_stable_under_inverse
added
def
category_theory.morphism_property.naturality_property
added
def
category_theory.morphism_property.stable_under_inverse