Commit 2022-08-16 04:11 3e0dd193

View on Github →

feat(category_theory): compute subobjects of structured arrows (#15912) One step closer to the Special Adjoint Functor Theorem.

Estimated changes

Modified src/category_theory/limits/comma.lean

added theorem category_theory.costructured_arrow.epi_iff_epi_left

added theorem category_theory.structured_arrow.mono_iff_mono_right

Modified src/category_theory/limits/over.lean

added theorem category_theory.over.epi_iff_epi_left

added theorem category_theory.over.epi_left_of_epi

added theorem category_theory.under.mono_iff_mono_right

added theorem category_theory.under.mono_right_of_mono

Modified src/category_theory/over.lean

added theorem category_theory.under.epi_of_epi_right

added theorem category_theory.under.mono_of_mono_right

Modified src/category_theory/structured_arrow.lean

added theorem category_theory.costructured_arrow.epi_of_epi_left

added theorem category_theory.costructured_arrow.ext

added theorem category_theory.costructured_arrow.ext_iff

added theorem category_theory.costructured_arrow.mono_of_mono_left

added theorem category_theory.structured_arrow.epi_of_epi_right

added theorem category_theory.structured_arrow.ext

added theorem category_theory.structured_arrow.ext_iff

added theorem category_theory.structured_arrow.mono_of_mono_right

Created src/category_theory/subobject/comma.lean

added theorem category_theory.costructured_arrow.lift_project_quotient

added def category_theory.costructured_arrow.lift_quotient

added def category_theory.costructured_arrow.project_quotient

added theorem category_theory.costructured_arrow.project_quotient_factors

added theorem category_theory.costructured_arrow.project_quotient_mk

added def category_theory.costructured_arrow.quotient_equiv

added theorem category_theory.costructured_arrow.unop_left_comp_of_mk_le_mk_unop

added theorem category_theory.costructured_arrow.unop_left_comp_underlying_iso_hom_unop

added theorem category_theory.structured_arrow.lift_project_subobject

added def category_theory.structured_arrow.lift_subobject

added def category_theory.structured_arrow.project_subobject

added theorem category_theory.structured_arrow.project_subobject_factors

added theorem category_theory.structured_arrow.project_subobject_mk

added def category_theory.structured_arrow.subobject_equiv