Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-08-31 20:38 72ce940c

View on Github →

feat(category_theory/limits/of_nat_iso): missing parts of the limits API (#1355)

feat(category_theory/limits/of_nat_isp)
Update src/category_theory/limits/limits.lean Co-Authored-By: Johan Commelin johan@commelin.net
Update src/category_theory/limits/limits.lean Co-Authored-By: Johan Commelin johan@commelin.net
use @[reassoc]
fixing after rename
fix renaming

Estimated changes

Modified src/category_theory/adjunction/limits.lean

Modified src/category_theory/limits/limits.lean

added def category_theory.limits.is_colimit.iso_unique_cocone_morphism

added theorem category_theory.limits.is_colimit.of_nat_iso.cocone_fac

added def category_theory.limits.is_colimit.of_nat_iso.cocone_of_hom

added theorem category_theory.limits.is_colimit.of_nat_iso.cocone_of_hom_fac

added theorem category_theory.limits.is_colimit.of_nat_iso.cocone_of_hom_of_cocone

added def category_theory.limits.is_colimit.of_nat_iso.colimit_cocone

added def category_theory.limits.is_colimit.of_nat_iso.hom_of_cocone

added theorem category_theory.limits.is_colimit.of_nat_iso.hom_of_cocone_of_hom

added def category_theory.limits.is_colimit.of_nat_iso

deleted def category_theory.limits.is_colimit.unique

added def category_theory.limits.is_colimit.unique_up_to_iso

deleted def category_theory.limits.is_colimit_iso_unique_cocone_morphism

added def category_theory.limits.is_limit.iso_unique_cone_morphism

added theorem category_theory.limits.is_limit.of_nat_iso.cone_fac

added def category_theory.limits.is_limit.of_nat_iso.cone_of_hom

added theorem category_theory.limits.is_limit.of_nat_iso.cone_of_hom_fac

added theorem category_theory.limits.is_limit.of_nat_iso.cone_of_hom_of_cone

added def category_theory.limits.is_limit.of_nat_iso.hom_of_cone

added theorem category_theory.limits.is_limit.of_nat_iso.hom_of_cone_of_hom

added def category_theory.limits.is_limit.of_nat_iso.limit_cone

added def category_theory.limits.is_limit.of_nat_iso

deleted def category_theory.limits.is_limit.unique

added def category_theory.limits.is_limit.unique_up_to_iso

deleted def category_theory.limits.is_limit_iso_unique_cone_morphism

Modified src/category_theory/limits/preserves.lean