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