Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-29 13:12 66ee65ca

View on Github →

feat(category): structured arrows (#6830) Factored out from #6820.

Estimated changes

Modified src/category_theory/elements.lean

deleted def category_theory.category_of_elements.comma_equivalence

deleted theorem category_theory.category_of_elements.comma_equivalence_functor

deleted theorem category_theory.category_of_elements.comma_equivalence_inverse

deleted def category_theory.category_of_elements.from_comma

deleted theorem category_theory.category_of_elements.from_comma_map

deleted theorem category_theory.category_of_elements.from_comma_obj

added def category_theory.category_of_elements.from_structured_arrow

added theorem category_theory.category_of_elements.from_structured_arrow_map

added theorem category_theory.category_of_elements.from_structured_arrow_obj

added def category_theory.category_of_elements.structured_arrow_equivalence

deleted def category_theory.category_of_elements.to_comma

deleted theorem category_theory.category_of_elements.to_comma_map

added theorem category_theory.category_of_elements.to_comma_map_right

deleted theorem category_theory.category_of_elements.to_comma_obj

added def category_theory.category_of_elements.to_structured_arrow

added theorem category_theory.category_of_elements.to_structured_arrow_obj

Modified src/category_theory/limits/cofinal.lean

Modified src/category_theory/over.lean

modified def category_theory.over

modified def category_theory.under

Created src/category_theory/structured_arrow.lean

added theorem category_theory.costructured_arrow.eq_mk

added def category_theory.costructured_arrow.hom_mk

added def category_theory.costructured_arrow.iso_mk

added def category_theory.costructured_arrow.map

added theorem category_theory.costructured_arrow.map_comp

added theorem category_theory.costructured_arrow.map_id

added theorem category_theory.costructured_arrow.map_mk

added def category_theory.costructured_arrow.mk

added theorem category_theory.costructured_arrow.mk_hom_eq_self

added def category_theory.costructured_arrow.mk_id_terminal

added theorem category_theory.costructured_arrow.mk_left

added theorem category_theory.costructured_arrow.mk_right

added def category_theory.costructured_arrow

added theorem category_theory.structured_arrow.eq_mk

added def category_theory.structured_arrow.hom_mk

added def category_theory.structured_arrow.iso_mk

added def category_theory.structured_arrow.map

added theorem category_theory.structured_arrow.map_comp

added theorem category_theory.structured_arrow.map_id

added theorem category_theory.structured_arrow.map_mk

added def category_theory.structured_arrow.mk

added theorem category_theory.structured_arrow.mk_hom_eq_self

added def category_theory.structured_arrow.mk_id_initial

added theorem category_theory.structured_arrow.mk_left

added theorem category_theory.structured_arrow.mk_right

added def category_theory.structured_arrow

Modified src/topology/sheaves/sheaf_condition/opens_le_cover.lean