Commit 2023-04-17 15:59 d8ef30e0

View on Github →

feat: port CategoryTheory.Subobject.Basic (#3444)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Category/Preorder.lean

Created Mathlib/CategoryTheory/Subobject/Basic.lean

added theorem CategoryTheory.Subobject.arrow_congr

added theorem CategoryTheory.Subobject.eq_mk_of_comm

added theorem CategoryTheory.Subobject.eq_of_comm

added theorem CategoryTheory.Subobject.eq_of_comp_arrow_eq

added def CategoryTheory.Subobject.existsPullbackAdj

added def CategoryTheory.Subobject.exists_

added theorem CategoryTheory.Subobject.exists_iso_map

added def CategoryTheory.Subobject.isoOfEq

added def CategoryTheory.Subobject.isoOfEqMk

added def CategoryTheory.Subobject.isoOfMkEq

added def CategoryTheory.Subobject.isoOfMkEqMk

added theorem CategoryTheory.Subobject.le_mk_of_comm

added theorem CategoryTheory.Subobject.le_of_comm

added def CategoryTheory.Subobject.lower

added def CategoryTheory.Subobject.lowerAdjunction

added def CategoryTheory.Subobject.lowerEquivalence

added theorem CategoryTheory.Subobject.lower_comm

added theorem CategoryTheory.Subobject.lower_iso

added def CategoryTheory.Subobject.lower₂

added def CategoryTheory.Subobject.map

added def CategoryTheory.Subobject.mapIso

added def CategoryTheory.Subobject.mapIsoToOrderIso

added theorem CategoryTheory.Subobject.mapIsoToOrderIso_apply

added theorem CategoryTheory.Subobject.mapIsoToOrderIso_symm_apply

added def CategoryTheory.Subobject.mapPullbackAdj

added theorem CategoryTheory.Subobject.map_comp

added theorem CategoryTheory.Subobject.map_id

added theorem CategoryTheory.Subobject.map_pullback

added def CategoryTheory.Subobject.mk

added theorem CategoryTheory.Subobject.mk_arrow

added theorem CategoryTheory.Subobject.mk_eq_mk_of_comm

added theorem CategoryTheory.Subobject.mk_eq_of_comm

added theorem CategoryTheory.Subobject.mk_le_mk_of_comm

added theorem CategoryTheory.Subobject.mk_le_of_comm

added def CategoryTheory.Subobject.ofLE

added def CategoryTheory.Subobject.ofLEMk

added theorem CategoryTheory.Subobject.ofLEMk_comp

added theorem CategoryTheory.Subobject.ofLEMk_comp_ofMkLE

added theorem CategoryTheory.Subobject.ofLEMk_comp_ofMkLEMk

added theorem CategoryTheory.Subobject.ofLE_arrow

added theorem CategoryTheory.Subobject.ofLE_comp_ofLE

added theorem CategoryTheory.Subobject.ofLE_comp_ofLEMk

added theorem CategoryTheory.Subobject.ofLE_mk_le_mk_of_comm

added theorem CategoryTheory.Subobject.ofLE_refl

added def CategoryTheory.Subobject.ofMkLE

added def CategoryTheory.Subobject.ofMkLEMk

added theorem CategoryTheory.Subobject.ofMkLEMk_comp

added theorem CategoryTheory.Subobject.ofMkLEMk_comp_ofMkLE

added theorem CategoryTheory.Subobject.ofMkLEMk_comp_ofMkLEMk

added theorem CategoryTheory.Subobject.ofMkLEMk_refl

added theorem CategoryTheory.Subobject.ofMkLE_arrow

added theorem CategoryTheory.Subobject.ofMkLE_comp_ofLE

added theorem CategoryTheory.Subobject.ofMkLE_comp_ofLEMk

added def CategoryTheory.Subobject.pullback

added theorem CategoryTheory.Subobject.pullback_comp

added theorem CategoryTheory.Subobject.pullback_id

added theorem CategoryTheory.Subobject.pullback_map_self

added theorem CategoryTheory.Subobject.representative_arrow

added theorem CategoryTheory.Subobject.representative_coe

added theorem CategoryTheory.Subobject.underlyingIso_arrow

added theorem CategoryTheory.Subobject.underlyingIso_hom_comp_eq_mk

added theorem CategoryTheory.Subobject.underlying_arrow

added def CategoryTheory.Subobject