Commit 2023-04-17 17:56 413c3422

View on Github →

feat: port CategoryTheory.Subobject.Lattice (#3447)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Subobject/Lattice.lean

added def CategoryTheory.MonoOver.botCoeIsoZero

added def CategoryTheory.MonoOver.botLe

added theorem CategoryTheory.MonoOver.bot_arrow

added theorem CategoryTheory.MonoOver.bot_arrow_eq_zero

added theorem CategoryTheory.MonoOver.bot_left

added def CategoryTheory.MonoOver.inf

added def CategoryTheory.MonoOver.infLeLeft

added def CategoryTheory.MonoOver.infLeRight

added def CategoryTheory.MonoOver.leInf

added def CategoryTheory.MonoOver.leSupLeft

added def CategoryTheory.MonoOver.leSupRight

added def CategoryTheory.MonoOver.leTop

added def CategoryTheory.MonoOver.mapBot

added def CategoryTheory.MonoOver.mapTop

added def CategoryTheory.MonoOver.pullbackSelf

added def CategoryTheory.MonoOver.pullbackTop

added def CategoryTheory.MonoOver.sup

added def CategoryTheory.MonoOver.supLe

added def CategoryTheory.MonoOver.topLePullbackSelf

added theorem CategoryTheory.MonoOver.top_arrow

added theorem CategoryTheory.MonoOver.top_left

added def CategoryTheory.Subobject.botCoeIsoInitial

added def CategoryTheory.Subobject.botCoeIsoZero

added theorem CategoryTheory.Subobject.bot_arrow

added theorem CategoryTheory.Subobject.bot_eq_initial_to

added theorem CategoryTheory.Subobject.bot_eq_zero

added theorem CategoryTheory.Subobject.bot_factors_iff_zero

added theorem CategoryTheory.Subobject.eq_top_of_isIso_arrow

added theorem CategoryTheory.Subobject.factors_left_of_inf_factors

added theorem CategoryTheory.Subobject.factors_right_of_inf_factors

added theorem CategoryTheory.Subobject.finset_inf_arrow_factors

added theorem CategoryTheory.Subobject.finset_inf_factors

added theorem CategoryTheory.Subobject.finset_sup_factors

added def CategoryTheory.Subobject.functor

added def CategoryTheory.Subobject.inf

added theorem CategoryTheory.Subobject.inf_arrow_factors_left

added theorem CategoryTheory.Subobject.inf_arrow_factors_right

added theorem CategoryTheory.Subobject.inf_def

added theorem CategoryTheory.Subobject.inf_eq_map_pullback'

added theorem CategoryTheory.Subobject.inf_eq_map_pullback

added theorem CategoryTheory.Subobject.inf_factors

added theorem CategoryTheory.Subobject.inf_le_left

added theorem CategoryTheory.Subobject.inf_le_right

added theorem CategoryTheory.Subobject.inf_map

added theorem CategoryTheory.Subobject.inf_pullback

added def CategoryTheory.Subobject.infₛ

added theorem CategoryTheory.Subobject.infₛ_le

added theorem CategoryTheory.Subobject.isIso_arrow_iff_eq_top

added theorem CategoryTheory.Subobject.isIso_iff_mk_eq_top

added def CategoryTheory.Subobject.leInfCone

added theorem CategoryTheory.Subobject.leInfCone_π_app_none

added theorem CategoryTheory.Subobject.le_inf

added theorem CategoryTheory.Subobject.le_infₛ

added theorem CategoryTheory.Subobject.le_supₛ

added theorem CategoryTheory.Subobject.map_bot

added theorem CategoryTheory.Subobject.map_top

added theorem CategoryTheory.Subobject.mk_eq_bot_iff_zero

added theorem CategoryTheory.Subobject.mk_eq_top_of_isIso

added theorem CategoryTheory.Subobject.nontrivial_of_not_isZero

added theorem CategoryTheory.Subobject.prod_eq_inf

added theorem CategoryTheory.Subobject.pullback_self

added theorem CategoryTheory.Subobject.pullback_top

added def CategoryTheory.Subobject.smallCoproductDesc

added def CategoryTheory.Subobject.subobjectOrderIso

added def CategoryTheory.Subobject.sup

added theorem CategoryTheory.Subobject.sup_factors_of_factors_left

added theorem CategoryTheory.Subobject.sup_factors_of_factors_right

added def CategoryTheory.Subobject.supₛ

added theorem CategoryTheory.Subobject.supₛ_le

added theorem CategoryTheory.Subobject.symm_apply_mem_iff_mem_image

added theorem CategoryTheory.Subobject.top_eq_id

added theorem CategoryTheory.Subobject.top_factors

added theorem CategoryTheory.Subobject.underlyingIso_inv_top_arrow

added theorem CategoryTheory.Subobject.underlyingIso_top_hom

added def CategoryTheory.Subobject.wideCospan

added theorem CategoryTheory.Subobject.wideCospan_map_term

added def CategoryTheory.Subobject.widePullback

added def CategoryTheory.Subobject.widePullbackι