Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-04 06:46 b57af8a5

View on Github →

feat(category_theory/basic/category): Combine and improve API on preorder categories. (#8982) Material on preorders as categories was previously scattered throughout the library. This PR unites this material into a single file category_theory/category/preorder and also expands upon it, by relating adjoints to galois connections.

Estimated changes

Modified src/category_theory/category/default.lean

deleted def category_theory.hom_of_le

deleted theorem category_theory.hom_of_le_comp

deleted theorem category_theory.hom_of_le_le_of_hom

deleted theorem category_theory.hom_of_le_refl

deleted theorem category_theory.le_of_hom

deleted theorem category_theory.le_of_hom_hom_of_le

Created src/category_theory/category/preorder.lean

added def category_theory.Preorder_to_Cat

added theorem category_theory.adjunction.gc

added def category_theory.equivalence.to_order_iso

added theorem category_theory.equivalence.to_order_iso_apply

added theorem category_theory.equivalence.to_order_iso_symm_apply

added theorem category_theory.functor.monotone

added def category_theory.hom_of_le

added theorem category_theory.hom_of_le_comp

added theorem category_theory.hom_of_le_le_of_hom

added theorem category_theory.hom_of_le_refl

added theorem category_theory.iso.to_eq

added theorem category_theory.le_of_hom

added theorem category_theory.le_of_hom_hom_of_le

added theorem category_theory.le_of_op_hom

added def category_theory.op_hom_of_le

added def galois_connection.adjunction

added def monotone.functor

added theorem monotone.functor_obj

Modified src/category_theory/equivalence.lean

deleted def category_theory.equivalence.to_order_iso

deleted theorem category_theory.equivalence.to_order_iso_apply

deleted theorem category_theory.equivalence.to_order_iso_symm_apply

Modified src/category_theory/filtered.lean

Modified src/category_theory/functor.lean

deleted theorem category_theory.functor.monotone

Modified src/category_theory/isomorphism.lean

deleted theorem category_theory.iso.to_eq

Modified src/category_theory/limits/lattice.lean

Modified src/category_theory/opposites.lean

deleted theorem category_theory.le_of_op_hom

deleted def category_theory.op_hom_of_le

Modified src/category_theory/skeletal.lean

Modified src/topology/category/Top/opens.lean