Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-11 04:03 0bd14ba9

View on Github →

feat(category_theory/limits/lattice): Add explicit formulas for limits in lattices (#9608) Add explicit descriptions of finite limits and colimits in complete lattices. In particular, the product and the pullback is equal to the infimum, while coproduct and pushout is the supremum. Furthermore, limit_iso_infi can be strengthened to an equality, as preorder categories are skeletal.

Estimated changes

Modified src/category_theory/limits/lattice.lean

modified def category_theory.limits.complete_lattice.colimit_cocone

added theorem category_theory.limits.complete_lattice.colimit_eq_supr

deleted def category_theory.limits.complete_lattice.colimit_iso_supr

deleted theorem category_theory.limits.complete_lattice.colimit_iso_supr_hom

deleted theorem category_theory.limits.complete_lattice.colimit_iso_supr_inv

added theorem category_theory.limits.complete_lattice.coprod_eq_sup

added def category_theory.limits.complete_lattice.finite_colimit_cocone

added theorem category_theory.limits.complete_lattice.finite_colimit_eq_finset_univ_sup

added theorem category_theory.limits.complete_lattice.finite_coproduct_eq_finset_sup

added def category_theory.limits.complete_lattice.finite_limit_cone

added theorem category_theory.limits.complete_lattice.finite_limit_eq_finset_univ_inf

added theorem category_theory.limits.complete_lattice.finite_product_eq_finset_inf

modified def category_theory.limits.complete_lattice.limit_cone

added theorem category_theory.limits.complete_lattice.limit_eq_infi

deleted def category_theory.limits.complete_lattice.limit_iso_infi

deleted theorem category_theory.limits.complete_lattice.limit_iso_infi_hom

deleted theorem category_theory.limits.complete_lattice.limit_iso_infi_inv

added theorem category_theory.limits.complete_lattice.prod_eq_inf

added theorem category_theory.limits.complete_lattice.pullback_eq_inf

added theorem category_theory.limits.complete_lattice.pushout_eq_sup