Mathlib Changelog
Changelog
About
Github
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