Lattice

📁 Source: Mathlib/CategoryTheory/Subobject/Lattice.lean

Statistics

Metric	Count
Definitions botCoeIsoZero, botLE, inf, infLELeft, infLERight, instBot, instInhabited, instTop, leInf, leSupLeft, leSupRight, leTop, mapBot, mapTop, pullbackSelf, pullbackTop, sup, supLe, topLEPullbackSelf, botCoeIsoInitial, botCoeIsoZero, boundedOrder, completeSemilatticeInf, completeSemilatticeSup, functor, inf, instCompleteLattice, instInhabited, instLattice, leInfCone, orderBot, orderTop, sInf, sSup, semilatticeInf, semilatticeSup, smallCoproductDesc, subobjectOrderIso, sup, wideCospan, widePullback, widePullbackι	42
Theorems bot_arrow, bot_arrow_eq_zero, bot_left, inf_map_app, inf_obj, initialTo_b_eq_zero, top_arrow, top_left, bot_arrow, bot_eq_initial_to, bot_eq_zero, bot_factors_iff_zero, epi_iff_mk_eq_top, eq_top_of_isIso_arrow, factors_left_of_inf_factors, factors_right_of_inf_factors, finset_inf_arrow_factors, finset_inf_factors, finset_sup_factors, functor_map, functor_obj, inf_arrow_factors_left, inf_arrow_factors_right, inf_comp_left, inf_comp_left_assoc, inf_comp_right, inf_comp_right_assoc, inf_def, inf_eq_map_pullback, inf_eq_map_pullback', inf_factors, inf_isPullback, inf_le_left, inf_le_right, inf_map, inf_pullback, isIso_arrow_iff_eq_top, isIso_iff_mk_eq_top, isIso_top_arrow, leInfCone_π_app_none, le_inf, le_sInf, le_sSup, map_bot, map_top, mk_eq_bot_iff_zero, mk_eq_top_of_isIso, nontrivial_of_not_isZero, prod_eq_inf, pullback_self, pullback_top, sInf_le, sSup_le, subsingleton_of_isInitial, subsingleton_of_isZero, sup_factors_of_factors_left, sup_factors_of_factors_right, symm_apply_mem_iff_mem_image, top_arrow_isIso, top_eq_id, top_factors, underlyingIso_inv_top_arrow, underlyingIso_inv_top_arrow_assoc, underlyingIso_top_hom, wideCospan_map_term, widePullbackι_mono	66
Total	108

CategoryTheory.MonoOver

Definitions

Name	Category	Theorems
botCoeIsoZero 📖	CompOp	—
botLE 📖	CompOp	—
inf 📖	CompOp	2 math math: inf_map_app, inf_obj
infLELeft 📖	CompOp	—
infLERight 📖	CompOp	—
instBot 📖	CompOp	3 math math: bot_left, bot_arrow, bot_arrow_eq_zero
instInhabited 📖	CompOp	—
instTop 📖	CompOp	2 math math: top_arrow, top_left
leInf 📖	CompOp	—
leSupLeft 📖	CompOp	—
leSupRight 📖	CompOp	—
leTop 📖	CompOp	—
mapBot 📖	CompOp	—
mapTop 📖	CompOp	—
pullbackSelf 📖	CompOp	—
pullbackTop 📖	CompOp	—
sup 📖	CompOp	—
supLe 📖	CompOp	—
topLEPullbackSelf 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bot_arrow 📖	mathematical	—	arrow Bot.bot CategoryTheory.MonoOver instBot CategoryTheory.Limits.initial.to	—	—
bot_arrow_eq_zero 📖	mathematical	—	arrow Bot.bot CategoryTheory.MonoOver instBot CategoryTheory.Limits.HasZeroObject.hasInitial CategoryTheory.Limits.HasZeroObject.initialMonoClass Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Limits.zero_of_source_iso_zero CategoryTheory.Limits.HasZeroObject.hasInitial CategoryTheory.Limits.HasZeroObject.initialMonoClass
bot_left 📖	mathematical	—	CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono Bot.bot CategoryTheory.MonoOver instBot CategoryTheory.Limits.initial	—	—
inf_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.MonoOver CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono CategoryTheory.Functor.comp CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.ObjectProperty.FullSubcategory.obj pullback arrow map mono CategoryTheory.Functor.map CategoryTheory.Functor CategoryTheory.Functor.category inf homMk CategoryTheory.Functor.obj CategoryTheory.Limits.pullback.lift CategoryTheory.Limits.pullback forget CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Limits.pullback.fst CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback.snd CategoryTheory.CommaMorphism.left CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory	—	mono
inf_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.MonoOver CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono CategoryTheory.Functor CategoryTheory.Functor.category inf CategoryTheory.Functor.comp CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.ObjectProperty.FullSubcategory.obj pullback arrow map mono	—	—
initialTo_b_eq_zero 📖	mathematical	—	CategoryTheory.Limits.initial.to CategoryTheory.Limits.HasZeroObject.hasInitial Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.initial CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Limits.HasZeroObject.hasInitial CategoryTheory.Limits.HasZeroObject.initialMonoClass bot_arrow bot_arrow_eq_zero
top_arrow 📖	mathematical	—	arrow Top.top CategoryTheory.MonoOver instTop CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
top_left 📖	mathematical	—	CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono Top.top CategoryTheory.MonoOver instTop	—	—

CategoryTheory.Subobject

Definitions

Name	Category	Theorems
botCoeIsoInitial 📖	CompOp	—
botCoeIsoZero 📖	CompOp	—
boundedOrder 📖	CompOp	2 math math: CategoryTheory.instIsSimpleOrderSubobjectOfSimple, CategoryTheory.simple_iff_subobject_isSimpleOrder
completeSemilatticeInf 📖	CompOp	—
completeSemilatticeSup 📖	CompOp	—
functor 📖	CompOp	2 math math: functor_obj, functor_map
inf 📖	CompOp	5 math math: inf_le_left, inf_eq_map_pullback', le_inf, inf_def, inf_le_right
instCompleteLattice 📖	CompOp	5 math math: CategoryTheory.IsGrothendieckAbelian.subobjectMk_of_isColimit_eq_iSup, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.exists_ordinal, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.functorToMonoOver_map, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.top_mem_range, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.functorToMonoOver_obj
instInhabited 📖	CompOp	—
instLattice 📖	CompOp	—
leInfCone 📖	CompOp	1 math math: leInfCone_π_app_none
orderBot 📖	CompOp	9 math math: bot_eq_initial_to, finset_sup_factors, bot_factors_iff_zero, CategoryTheory.Limits.imageSubobject_zero, CategoryTheory.subobject_simple_iff_isAtom, map_bot, mk_eq_bot_iff_zero, bot_arrow, bot_eq_zero
orderTop 📖	CompOp	29 math math: AlgebraicTopology.NormalizedMooreComplex.obj_d, top_arrow_isIso, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.exists_ordinal, map_top, isIso_top_arrow, CategoryTheory.ObjectProperty.IsStrongGenerator.subobject_eq_top, CategoryTheory.ExtremalEpi.subobject_eq_top, CategoryTheory.Dial.tensorUnit_rel, finset_inf_factors, mk_eq_top_of_isIso, top_eq_id, CategoryTheory.Limits.equalizerSubobject_of_self, top_factors, eq_top_of_isIso_arrow, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.top_mem_range, underlyingIso_inv_top_arrow_assoc, isIso_arrow_iff_eq_top, AlgebraicTopology.NormalizedMooreComplex.objX_add_one, underlyingIso_inv_top_arrow, underlyingIso_top_hom, AlgebraicTopology.NormalizedMooreComplex.objX_zero, pullback_top, epi_iff_mk_eq_top, isIso_iff_mk_eq_top, pullback_self, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.largerSubobject_top, finset_inf_arrow_factors, CategoryTheory.Dial.tensorUnitImpl_rel, CategoryTheory.Limits.kernelSubobject_zero
sInf 📖	CompOp	2 math math: le_sInf, sInf_le
sSup 📖	CompOp	2 math math: le_sSup, sSup_le
semilatticeInf 📖	CompOp	26 math math: AlgebraicTopology.NormalizedMooreComplex.obj_d, CategoryTheory.Dial.tensorObjImpl_rel, inf_eq_of_isDetecting, CategoryTheory.Regular.frobeniusStrongEpiMonoFactorisation_I, inf_comp_left, inf_arrow_factors_right, prod_eq_inf, inf_isPullback, CategoryTheory.Regular.instIsRegularEpiFrobeniusMorphism, CategoryTheory.Regular.frobeniusStrongEpiMonoFactorisation_e, inf_factors, finset_inf_factors, inf_map, CategoryTheory.Regular.exists_inf_pullback_eq_exists_inf, inf_def, inf_arrow_factors_left, CategoryTheory.Regular.frobeniusMorphism_isPullback, AlgebraicTopology.NormalizedMooreComplex.objX_add_one, CategoryTheory.Regular.frobeniusStrongEpiMonoFactorisation_m, inf_comp_left_assoc, inf_comp_right, inf_eq_map_pullback, inf_pullback, inf_comp_right_assoc, finset_inf_arrow_factors, CategoryTheory.Dial.tensorObj_rel
semilatticeSup 📖	CompOp	3 math math: finset_sup_factors, sup_factors_of_factors_left, sup_factors_of_factors_right
smallCoproductDesc 📖	CompOp	—
subobjectOrderIso 📖	CompOp	—
sup 📖	CompOp	—
wideCospan 📖	CompOp	2 math math: wideCospan_map_term, leInfCone_π_app_none
widePullback 📖	CompOp	1 math math: widePullbackι_mono
widePullbackι 📖	CompOp	1 math math: widePullbackι_mono

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bot_arrow 📖	mathematical	—	arrow Bot.bot CategoryTheory.Subobject OrderBot.toBot Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject orderBot CategoryTheory.Limits.HasZeroObject.hasInitial CategoryTheory.Limits.HasZeroObject.initialMonoClass Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory underlying CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Limits.zero_of_source_iso_zero CategoryTheory.Limits.HasZeroObject.hasInitial CategoryTheory.Limits.HasZeroObject.initialMonoClass
bot_eq_initial_to 📖	mathematical	—	Bot.bot CategoryTheory.Subobject OrderBot.toBot Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject orderBot CategoryTheory.Limits.initial CategoryTheory.Limits.initial.to CategoryTheory.Limits.initial.mono_from	—	—
bot_eq_zero 📖	mathematical	—	Bot.bot CategoryTheory.Subobject OrderBot.toBot Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject orderBot CategoryTheory.Limits.HasZeroObject.hasInitial CategoryTheory.Limits.HasZeroObject.initialMonoClass CategoryTheory.Limits.HasZeroObject.zero' Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.HasZeroObject.instMono	—	mk_eq_mk_of_comm CategoryTheory.Limits.HasZeroObject.hasInitial CategoryTheory.Limits.HasZeroObject.initialMonoClass CategoryTheory.Limits.HasZeroObject.instMono CategoryTheory.Limits.comp_zero CategoryTheory.MonoOver.initialTo_b_eq_zero
bot_factors_iff_zero 📖	mathematical	—	Factors Bot.bot CategoryTheory.Subobject OrderBot.toBot Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject orderBot CategoryTheory.Limits.HasZeroObject.hasInitial CategoryTheory.Limits.HasZeroObject.initialMonoClass Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Limits.HasZeroObject.hasInitial CategoryTheory.Limits.HasZeroObject.initialMonoClass CategoryTheory.MonoOver.bot_arrow_eq_zero CategoryTheory.Limits.comp_zero CategoryTheory.MonoOver.initialTo_b_eq_zero
epi_iff_mk_eq_top 📖	mathematical	—	CategoryTheory.Epi Top.top CategoryTheory.Subobject OrderTop.toTop Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject orderTop	—	isIso_iff_mk_eq_top CategoryTheory.isIso_of_mono_of_epi CategoryTheory.epi_of_strongEpi CategoryTheory.strongEpi_of_isIso
eq_top_of_isIso_arrow 📖	mathematical	—	Top.top CategoryTheory.Subobject OrderTop.toTop Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject orderTop	—	isIso_arrow_iff_eq_top
factors_left_of_inf_factors 📖	—	Factors CategoryTheory.Subobject SemilatticeInf.toMin semilatticeInf	—	—	factors_of_le inf_le_left
factors_right_of_inf_factors 📖	—	Factors CategoryTheory.Subobject SemilatticeInf.toMin semilatticeInf	—	—	factors_of_le inf_le_right
finset_inf_arrow_factors 📖	mathematical	Finset Finset.instMembership	Factors CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject underlying Finset.inf semilatticeInf orderTop arrow	—	Finset.induction_on Finset.inf_insert inf_arrow_factors_left factorThru_arrow factors_comp_arrow inf_arrow_factors_right factors_of_factors_right
finset_inf_factors 📖	mathematical	—	Factors Finset.inf CategoryTheory.Subobject semilatticeInf orderTop	—	Finset.induction_on instIsEmptyFalse Finset.inf_insert
finset_sup_factors 📖	mathematical	Finset Finset.instMembership Factors	Finset.sup CategoryTheory.Subobject semilatticeSup orderBot	—	Finset.induction_on Finset.sup_insert sup_factors_of_factors_left sup_factors_of_factors_right
functor_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.types functor CategoryTheory.Functor.obj CategoryTheory.Subobject Opposite.unop Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject pullback Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
functor_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types functor CategoryTheory.Subobject Opposite.unop	—	—
inf_arrow_factors_left 📖	mathematical	—	Factors CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject underlying SemilatticeInf.toMin semilatticeInf arrow	—	factors_iff inf_le_left ofLE_arrow
inf_arrow_factors_right 📖	mathematical	—	Factors CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject underlying SemilatticeInf.toMin semilatticeInf arrow	—	factors_iff inf_le_right ofLE_arrow
inf_comp_left 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject underlying SemilatticeInf.toMin semilatticeInf ofLE arrow	—	ofLE_arrow inf_le_left
inf_comp_left_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject underlying SemilatticeInf.toMin semilatticeInf ofLE arrow	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inf_comp_left
inf_comp_right 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject underlying SemilatticeInf.toMin semilatticeInf ofLE arrow	—	ofLE_arrow inf_le_right
inf_comp_right_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject underlying SemilatticeInf.toMin semilatticeInf ofLE arrow	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inf_comp_right
inf_def 📖	mathematical	—	CategoryTheory.Subobject SemilatticeInf.toMin semilatticeInf CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Functor CategoryTheory.Functor.category inf	—	—
inf_eq_map_pullback 📖	mathematical	—	CategoryTheory.Subobject SemilatticeInf.toMin semilatticeInf Quotient.mk'' CategoryTheory.MonoOver CategoryTheory.isIsomorphicSetoid CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.ObjectProperty.FullSubcategory.obj Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject map CategoryTheory.MonoOver.arrow CategoryTheory.MonoOver.mono pullback	—	inf_eq_map_pullback'
inf_eq_map_pullback' 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Functor CategoryTheory.Functor.category inf Quotient.mk'' CategoryTheory.MonoOver CategoryTheory.isIsomorphicSetoid CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.ObjectProperty.FullSubcategory.obj map CategoryTheory.MonoOver.arrow CategoryTheory.MonoOver.mono pullback	—	Quotient.inductionOn' CategoryTheory.MonoOver.mono
inf_factors 📖	mathematical	—	Factors CategoryTheory.Subobject SemilatticeInf.toMin semilatticeInf	—	factors_left_of_inf_factors factors_right_of_inf_factors Quotient.ind₂' CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.pullback.lift_snd_assoc
inf_isPullback 📖	mathematical	—	CategoryTheory.IsPullback CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject underlying SemilatticeInf.toMin semilatticeInf ofLE arrow	—	ofLE_arrow CategoryTheory.CommSq.w factors_comp_arrow CategoryTheory.Limits.PullbackCone.condition eq_of_comp_arrow_eq CategoryTheory.Category.assoc factorThru_arrow factorThru.congr_simp factorThru_comp_arrow
inf_le_left 📖	mathematical	—	CategoryTheory.Subobject Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Functor.obj Preorder.smallCategory CategoryTheory.Functor CategoryTheory.Functor.category inf	—	Quotient.inductionOn₂'
inf_le_right 📖	mathematical	—	CategoryTheory.Subobject Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Functor.obj Preorder.smallCategory CategoryTheory.Functor CategoryTheory.Functor.category inf	—	Quotient.inductionOn₂'
inf_map 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject map SemilatticeInf.toMin semilatticeInf	—	Quotient.ind' inf_def CategoryTheory.MonoOver.mono inf_eq_map_pullback' CategoryTheory.mono_comp map_comp pullback_comp pullback_map_self
inf_pullback 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject pullback SemilatticeInf.toMin semilatticeInf	—	Quotient.ind' inf_def CategoryTheory.MonoOver.mono inf_eq_map_pullback' pullback_comp CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.pullback.snd_of_mono map_pullback CategoryTheory.Limits.pullback.condition
isIso_arrow_iff_eq_top 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject underlying arrow Top.top OrderTop.toTop Preorder.toLE orderTop	—	arrow_mono isIso_iff_mk_eq_top mk_arrow
isIso_iff_mk_eq_top 📖	mathematical	—	CategoryTheory.IsIso Top.top CategoryTheory.Subobject OrderTop.toTop Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject orderTop	—	mk_eq_mk_of_comm CategoryTheory.instMonoId CategoryTheory.Category.comp_id Eq.le ofMkLEMk_comp CategoryTheory.Iso.isIso_hom
isIso_top_arrow 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject underlying Top.top OrderTop.toTop Preorder.toLE orderTop arrow	—	isIso_arrow_iff_eq_top
leInfCone_π_app_none 📖	mathematical	CategoryTheory.Subobject Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject	CategoryTheory.NatTrans.app CategoryTheory.Limits.WidePullbackShape Set.Elem Shrink CategoryTheory.small_subobject Set.image DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike equivShrink CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt wideCospan leInfCone CategoryTheory.Limits.Cone.π arrow	—	CategoryTheory.small_subobject
le_inf 📖	mathematical	CategoryTheory.Subobject Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject	CategoryTheory.Functor.obj Preorder.smallCategory CategoryTheory.Functor CategoryTheory.Functor.category inf	—	Quotient.inductionOn₃'
le_sInf 📖	mathematical	CategoryTheory.Limits.HasWidePullbacks CategoryTheory.Subobject Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject	sInf	—	le_of_comm CategoryTheory.small_subobject CategoryTheory.Limits.hasLimitOfHasLimitsOfShape widePullbackι_mono CategoryTheory.Category.assoc underlyingIso_arrow widePullbackι.eq_1 CategoryTheory.Limits.limit.lift_π leInfCone_π_app_none
le_sSup 📖	mathematical	CategoryTheory.Limits.HasCoproducts CategoryTheory.Subobject Set Set.instMembership	Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject sSup	—	le_of_comm CategoryTheory.small_subobject Equiv.symm_apply_apply CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Category.assoc underlyingIso_arrow CategoryTheory.Limits.image.fac CategoryTheory.Limits.colimit.ι_desc arrow_congr
map_bot 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject map Bot.bot OrderBot.toBot Preorder.toLE orderBot	—	Quotient.sound'
map_top 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject map Top.top OrderTop.toTop Preorder.toLE orderTop	—	Quotient.sound'
mk_eq_bot_iff_zero 📖	mathematical	—	Bot.bot CategoryTheory.Subobject OrderBot.toBot Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject orderBot CategoryTheory.Limits.HasZeroObject.hasInitial CategoryTheory.Limits.HasZeroObject.initialMonoClass Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Limits.HasZeroObject.hasInitial CategoryTheory.Limits.HasZeroObject.initialMonoClass mk_factors_self mk_eq_mk_of_comm CategoryTheory.Limits.isoZeroOfMonoEqZero.congr_simp CategoryTheory.Limits.HasZeroObject.zeroIsoInitial_hom CategoryTheory.Limits.comp_zero CategoryTheory.MonoOver.initialTo_b_eq_zero
mk_eq_top_of_isIso 📖	mathematical	—	CategoryTheory.mono_of_strongMono CategoryTheory.strongMono_of_isIso Top.top CategoryTheory.Subobject OrderTop.toTop Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject orderTop	—	CategoryTheory.mono_of_strongMono CategoryTheory.strongMono_of_isIso isIso_iff_mk_eq_top
nontrivial_of_not_isZero 📖	mathematical	CategoryTheory.Limits.IsZero	Nontrivial CategoryTheory.Subobject	—	CategoryTheory.Limits.HasZeroObject.instMono CategoryTheory.instMonoId CategoryTheory.Limits.IsZero.of_iso CategoryTheory.Limits.isZero_zero
prod_eq_inf 📖	mathematical	—	CategoryTheory.Limits.prod CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject SemilatticeInf.toMin semilatticeInf	—	le_antisymm le_inf CategoryTheory.leOfHom inf_le_left inf_le_right
pullback_self 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject pullback Top.top OrderTop.toTop Preorder.toLE orderTop	—	Quotient.sound'
pullback_top 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject pullback Top.top OrderTop.toTop Preorder.toLE orderTop	—	Quotient.sound'
sInf_le 📖	mathematical	CategoryTheory.Limits.HasWidePullbacks CategoryTheory.Subobject Set Set.instMembership	Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject sInf	—	le_of_comm widePullbackι_mono CategoryTheory.small_subobject Set.mem_image_of_mem CategoryTheory.Limits.hasLimitOfHasLimitsOfShape Equiv.symm_apply_apply CategoryTheory.Category.assoc arrow_congr CategoryTheory.Limits.limit.w
sSup_le 📖	mathematical	CategoryTheory.Limits.HasCoproducts CategoryTheory.Subobject Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject	sSup	—	le_of_comm CategoryTheory.small_subobject arrow_mono CategoryTheory.Limits.Sigma.hom_ext CategoryTheory.Limits.colimit.ι_desc_assoc underlying_arrow CategoryTheory.Limits.colimit.ι_desc CategoryTheory.Category.assoc CategoryTheory.Limits.image.lift_fac
subsingleton_of_isInitial 📖	mathematical	—	CategoryTheory.Subobject	—	CategoryTheory.instMonoId mk_surjective CategoryTheory.Limits.IsInitial.hom_ext CategoryTheory.cancel_mono CategoryTheory.Category.assoc CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id mk_eq_mk_of_comm
subsingleton_of_isZero 📖	mathematical	CategoryTheory.Limits.IsZero	CategoryTheory.Subobject	—	subsingleton_of_isInitial
sup_factors_of_factors_left 📖	mathematical	Factors	CategoryTheory.Subobject SemilatticeSup.toMax semilatticeSup	—	factors_of_le le_sup_left
sup_factors_of_factors_right 📖	mathematical	Factors	CategoryTheory.Subobject SemilatticeSup.toMax semilatticeSup	—	factors_of_le le_sup_right
symm_apply_mem_iff_mem_image 📖	mathematical	—	Set Set.instMembership DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm Set.image	—	Equiv.apply_symm_apply Equiv.symm_apply_apply
top_arrow_isIso 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject underlying Top.top OrderTop.toTop Preorder.toLE orderTop arrow	—	CategoryTheory.instMonoId underlyingIso_top_hom CategoryTheory.Iso.isIso_hom
top_eq_id 📖	mathematical	—	Top.top CategoryTheory.Subobject OrderTop.toTop Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject orderTop CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.instMonoId	—	—
top_factors 📖	mathematical	—	Factors Top.top CategoryTheory.Subobject OrderTop.toTop Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject orderTop	—	CategoryTheory.Category.comp_id
underlyingIso_inv_top_arrow 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject underlying CategoryTheory.CategoryStruct.id CategoryTheory.instMonoId CategoryTheory.Iso.inv underlyingIso arrow Top.top OrderTop.toTop Preorder.toLE orderTop	—	underlyingIso_arrow CategoryTheory.instMonoId
underlyingIso_inv_top_arrow_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject underlying CategoryTheory.CategoryStruct.id CategoryTheory.instMonoId CategoryTheory.Iso.inv underlyingIso arrow Top.top OrderTop.toTop Preorder.toLE orderTop	—	CategoryTheory.instMonoId CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' underlyingIso_inv_top_arrow
underlyingIso_top_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject underlying CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.instMonoId underlyingIso arrow Top.top OrderTop.toTop Preorder.toLE orderTop	—	CategoryTheory.instMonoId CategoryTheory.Category.comp_id
wideCospan_map_term 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Limits.WidePullbackShape Set.Elem Shrink CategoryTheory.Subobject CategoryTheory.small_subobject Set.image DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike equivShrink CategoryTheory.Limits.WidePullbackShape.category wideCospan CategoryTheory.Limits.WidePullbackShape.Hom.term arrow Equiv.symm Set Set.instMembership	—	CategoryTheory.small_subobject
widePullbackι_mono 📖	mathematical	CategoryTheory.Limits.HasWidePullbacks	CategoryTheory.Mono widePullback widePullbackι	—	CategoryTheory.Limits.limit.hom_ext CategoryTheory.small_subobject CategoryTheory.cancel_mono arrow_mono CategoryTheory.Category.assoc CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.limit.w

---

← Back to Index