PartOrdEmb

📁 Source: Mathlib/Order/Category/PartOrdEmb.lean

Statistics

Metric	Count
Definitions `PartOrdEmb`, `hom`, `hom`, `hom'`, `mk`, `CoconePt`, `desc`, `cocone`, `instPartialOrderCoconePt`, `isColimitCocone`, `carrier`, `dual`, `dualEquiv`, `hasForgetToPartOrd`, `instCategory`, `instCoeSortType`, `instConcreteCategoryOrderEmbeddingCarrier`, `ofHom`, `str`	19
Theorems `ext`, `ext_iff`, `injective`, `le_iff_le`, `mk_hom`, `mk_inv`, `fac_apply`, `cocone_pt_coe`, `cocone_ι_app`, `instHasColimit`, `instHasColimitsOfShape`, `instHasFilteredColimitsOfSize`, `instPreservesColimitForgetOrderEmbeddingCarrier`, `instPreservesColimitsOfShapeForgetOrderEmbeddingCarrier`, `instPreservesFilteredColimitsOfSizeForgetOrderEmbeddingCarrier`, `coe_comp`, `coe_id`, `coe_of`, `comp_apply`, `dualEquiv_functor`, `dualEquiv_inverse`, `dual_map`, `ext`, `ext_iff`, `forget_map`, `hom_comp`, `hom_ext`, `hom_ext_iff`, `hom_id`, `hom_inv_apply`, `hom_ofHom`, `id_apply`, `inv_hom_apply`, `ofHom_apply`, `ofHom_comp`, `ofHom_hom`, `ofHom_id`, `partOrdEmb_dual_comp_forget_to_pardOrd`	38
Total	57

PartOrdEmb

Definitions

Name	Category	Theorems
`carrier` 📖	CompOp	25 math math: `Limits.cocone_pt_coe`, `ofHom_hom`, `comp_apply`, `hom_inv_apply`, `hom_comp`, `Limits.CoconePt.fac_apply`, `ofHom_apply`, `Limits.cocone_ι_app`, `dual_map`, `hom_id`, `partOrdEmb_dual_comp_forget_to_pardOrd`, `coe_comp`, `inv_hom_apply`, `id_apply`, `forget_map`, `coe_of`, `Limits.instPreservesColimitsOfShapeForgetOrderEmbeddingCarrier`, `Hom.injective`, `Hom.le_iff_le`, `Iso.mk_hom`, `Limits.instPreservesFilteredColimitsOfSizeForgetOrderEmbeddingCarrier`, `ext_iff`, `Limits.instPreservesColimitForgetOrderEmbeddingCarrier`, `coe_id`, `Iso.mk_inv`
`dual` 📖	CompOp	4 math math: `dual_map`, `partOrdEmb_dual_comp_forget_to_pardOrd`, `dualEquiv_inverse`, `dualEquiv_functor`
`dualEquiv` 📖	CompOp	2 math math: `dualEquiv_inverse`, `dualEquiv_functor`
`hasForgetToPartOrd` 📖	CompOp	1 math math: `partOrdEmb_dual_comp_forget_to_pardOrd`
`instCategory` 📖	CompOp	30 math math: `Limits.cocone_pt_coe`, `comp_apply`, `hom_inv_apply`, `hom_comp`, `Limits.CoconePt.fac_apply`, `ofHom_apply`, `Limits.cocone_ι_app`, `Limits.instHasColimit`, `dual_map`, `hom_id`, `ofHom_id`, `partOrdEmb_dual_comp_forget_to_pardOrd`, `dualEquiv_inverse`, `coe_comp`, `inv_hom_apply`, `id_apply`, `forget_map`, `Limits.instPreservesColimitsOfShapeForgetOrderEmbeddingCarrier`, `Hom.injective`, `ofHom_comp`, `Hom.le_iff_le`, `Limits.instHasColimitsOfShape`, `Iso.mk_hom`, `dualEquiv_functor`, `Limits.instPreservesFilteredColimitsOfSizeForgetOrderEmbeddingCarrier`, `ext_iff`, `Limits.instPreservesColimitForgetOrderEmbeddingCarrier`, `Limits.instHasFilteredColimitsOfSize`, `coe_id`, `Iso.mk_inv`
`instCoeSortType` 📖	CompOp	—
`instConcreteCategoryOrderEmbeddingCarrier` 📖	CompOp	17 math math: `comp_apply`, `hom_inv_apply`, `Limits.CoconePt.fac_apply`, `ofHom_apply`, `Limits.cocone_ι_app`, `partOrdEmb_dual_comp_forget_to_pardOrd`, `coe_comp`, `inv_hom_apply`, `id_apply`, `forget_map`, `Limits.instPreservesColimitsOfShapeForgetOrderEmbeddingCarrier`, `Hom.injective`, `Hom.le_iff_le`, `Limits.instPreservesFilteredColimitsOfSizeForgetOrderEmbeddingCarrier`, `ext_iff`, `Limits.instPreservesColimitForgetOrderEmbeddingCarrier`, `coe_id`
`ofHom` 📖	CompOp	9 math math: `ofHom_hom`, `ofHom_apply`, `Limits.cocone_ι_app`, `dual_map`, `ofHom_id`, `hom_ofHom`, `ofHom_comp`, `Iso.mk_hom`, `Iso.mk_inv`
`str` 📖	CompOp	23 math math: `ofHom_hom`, `comp_apply`, `hom_inv_apply`, `hom_comp`, `Limits.CoconePt.fac_apply`, `ofHom_apply`, `Limits.cocone_ι_app`, `dual_map`, `hom_id`, `partOrdEmb_dual_comp_forget_to_pardOrd`, `coe_comp`, `inv_hom_apply`, `id_apply`, `forget_map`, `Limits.instPreservesColimitsOfShapeForgetOrderEmbeddingCarrier`, `Hom.injective`, `Hom.le_iff_le`, `Iso.mk_hom`, `Limits.instPreservesFilteredColimitsOfSizeForgetOrderEmbeddingCarrier`, `ext_iff`, `Limits.instPreservesColimitForgetOrderEmbeddingCarrier`, `coe_id`, `Iso.mk_inv`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_comp` 📖	mathematical	—	`DFunLike.coe` `carrier` `CategoryTheory.ConcreteCategory.hom` `PartOrdEmb` `instCategory` `OrderEmbedding` `Preorder.toLE` `PartialOrder.toPreorder` `str` `instFunLikeOrderEmbedding` `instConcreteCategoryOrderEmbeddingCarrier` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	—	—
`coe_id` 📖	mathematical	—	`DFunLike.coe` `carrier` `CategoryTheory.ConcreteCategory.hom` `PartOrdEmb` `instCategory` `OrderEmbedding` `Preorder.toLE` `PartialOrder.toPreorder` `str` `instFunLikeOrderEmbedding` `instConcreteCategoryOrderEmbeddingCarrier` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	—
`coe_of` 📖	mathematical	—	`carrier` `of`	—	—
`comp_apply` 📖	mathematical	—	`DFunLike.coe` `carrier` `CategoryTheory.ConcreteCategory.hom` `PartOrdEmb` `instCategory` `OrderEmbedding` `Preorder.toLE` `PartialOrder.toPreorder` `str` `instFunLikeOrderEmbedding` `instConcreteCategoryOrderEmbeddingCarrier` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	—	—
`dualEquiv_functor` 📖	mathematical	—	`CategoryTheory.Equivalence.functor` `PartOrdEmb` `instCategory` `dualEquiv` `dual`	—	—
`dualEquiv_inverse` 📖	mathematical	—	`CategoryTheory.Equivalence.inverse` `PartOrdEmb` `instCategory` `dualEquiv` `dual`	—	—
`dual_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `PartOrdEmb` `instCategory` `dual` `ofHom` `OrderDual` `carrier` `OrderDual.instPartialOrder` `str` `OrderEmbedding.dual` `PartialOrder.toPreorder` `Hom.hom`	—	—
`ext` 📖	—	`DFunLike.coe` `carrier` `CategoryTheory.ConcreteCategory.hom` `PartOrdEmb` `instCategory` `OrderEmbedding` `Preorder.toLE` `PartialOrder.toPreorder` `str` `instFunLikeOrderEmbedding` `instConcreteCategoryOrderEmbeddingCarrier`	—	—	`CategoryTheory.ConcreteCategory.hom_ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `carrier` `CategoryTheory.ConcreteCategory.hom` `PartOrdEmb` `instCategory` `OrderEmbedding` `Preorder.toLE` `PartialOrder.toPreorder` `str` `instFunLikeOrderEmbedding` `instConcreteCategoryOrderEmbeddingCarrier`	—	`ext`
`forget_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `PartOrdEmb` `instCategory` `CategoryTheory.types` `CategoryTheory.forget` `OrderEmbedding` `carrier` `Preorder.toLE` `PartialOrder.toPreorder` `str` `instFunLikeOrderEmbedding` `instConcreteCategoryOrderEmbeddingCarrier` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom`	—	—
`hom_comp` 📖	mathematical	—	`Hom.hom` `CategoryTheory.CategoryStruct.comp` `PartOrdEmb` `CategoryTheory.Category.toCategoryStruct` `instCategory` `RelEmbedding.trans` `carrier` `Preorder.toLE` `PartialOrder.toPreorder` `str`	—	—
`hom_ext` 📖	—	`Hom.hom`	—	—	`Hom.ext`
`hom_ext_iff` 📖	mathematical	—	`Hom.hom`	—	`hom_ext`
`hom_id` 📖	mathematical	—	`Hom.hom` `CategoryTheory.CategoryStruct.id` `PartOrdEmb` `CategoryTheory.Category.toCategoryStruct` `instCategory` `RelEmbedding.refl` `carrier` `Preorder.toLE` `PartialOrder.toPreorder` `str`	—	—
`hom_inv_apply` 📖	mathematical	—	`DFunLike.coe` `carrier` `CategoryTheory.ConcreteCategory.hom` `PartOrdEmb` `instCategory` `OrderEmbedding` `Preorder.toLE` `PartialOrder.toPreorder` `str` `instFunLikeOrderEmbedding` `instConcreteCategoryOrderEmbeddingCarrier` `CategoryTheory.Iso.hom` `CategoryTheory.Iso.inv`	—	`CategoryTheory.Iso.inv_hom_id_apply`
`hom_ofHom` 📖	mathematical	—	`Hom.hom` `of` `ofHom`	—	—
`id_apply` 📖	mathematical	—	`DFunLike.coe` `carrier` `CategoryTheory.ConcreteCategory.hom` `PartOrdEmb` `instCategory` `OrderEmbedding` `Preorder.toLE` `PartialOrder.toPreorder` `str` `instFunLikeOrderEmbedding` `instConcreteCategoryOrderEmbeddingCarrier` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	`CategoryTheory.id_apply`
`inv_hom_apply` 📖	mathematical	—	`DFunLike.coe` `carrier` `CategoryTheory.ConcreteCategory.hom` `PartOrdEmb` `instCategory` `OrderEmbedding` `Preorder.toLE` `PartialOrder.toPreorder` `str` `instFunLikeOrderEmbedding` `instConcreteCategoryOrderEmbeddingCarrier` `CategoryTheory.Iso.inv` `CategoryTheory.Iso.hom`	—	`CategoryTheory.Iso.hom_inv_id_apply`
`ofHom_apply` 📖	mathematical	—	`DFunLike.coe` `of` `carrier` `CategoryTheory.ConcreteCategory.hom` `PartOrdEmb` `instCategory` `OrderEmbedding` `Preorder.toLE` `PartialOrder.toPreorder` `str` `instFunLikeOrderEmbedding` `instConcreteCategoryOrderEmbeddingCarrier` `ofHom`	—	—
`ofHom_comp` 📖	mathematical	—	`ofHom` `RelEmbedding.trans` `Preorder.toLE` `PartialOrder.toPreorder` `CategoryTheory.CategoryStruct.comp` `PartOrdEmb` `CategoryTheory.Category.toCategoryStruct` `instCategory` `of`	—	—
`ofHom_hom` 📖	mathematical	—	`ofHom` `carrier` `str` `Hom.hom`	—	—
`ofHom_id` 📖	mathematical	—	`ofHom` `RelEmbedding.refl` `Preorder.toLE` `PartialOrder.toPreorder` `CategoryTheory.CategoryStruct.id` `PartOrdEmb` `CategoryTheory.Category.toCategoryStruct` `instCategory` `of`	—	—

PartOrdEmb.Hom

Definitions

Name	Category	Theorems
`hom` 📖	CompOp	6 math math: `PartOrdEmb.ofHom_hom`, `PartOrdEmb.hom_comp`, `PartOrdEmb.dual_map`, `PartOrdEmb.hom_id`, `PartOrdEmb.hom_ext_iff`, `PartOrdEmb.hom_ofHom`
`hom'` 📖	CompOp	1 math math: `ext_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`hom'`	—	—	—
`ext_iff` 📖	mathematical	—	`hom'`	—	`ext`
`injective` 📖	mathematical	—	`PartOrdEmb.carrier` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `PartOrdEmb` `PartOrdEmb.instCategory` `OrderEmbedding` `Preorder.toLE` `PartialOrder.toPreorder` `PartOrdEmb.str` `instFunLikeOrderEmbedding` `PartOrdEmb.instConcreteCategoryOrderEmbeddingCarrier`	—	`RelEmbedding.injective`
`le_iff_le` 📖	mathematical	—	`PartOrdEmb.carrier` `Preorder.toLE` `PartialOrder.toPreorder` `PartOrdEmb.str` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `PartOrdEmb` `PartOrdEmb.instCategory` `OrderEmbedding` `instFunLikeOrderEmbedding` `PartOrdEmb.instConcreteCategoryOrderEmbeddingCarrier`	—	`OrderEmbedding.le_iff_le`

PartOrdEmb.Hom.Simps

Definitions

Name	Category	Theorems
`hom` 📖	CompOp	—

PartOrdEmb.Iso

Definitions

Name	Category	Theorems
`mk` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mk_hom` 📖	mathematical	—	`CategoryTheory.Iso.hom` `PartOrdEmb` `PartOrdEmb.instCategory` `PartOrdEmb.ofHom` `PartOrdEmb.carrier` `PartOrdEmb.str` `RelIso.toRelEmbedding` `Preorder.toLE` `PartialOrder.toPreorder`	—	—
`mk_inv` 📖	mathematical	—	`CategoryTheory.Iso.inv` `PartOrdEmb` `PartOrdEmb.instCategory` `PartOrdEmb.ofHom` `PartOrdEmb.carrier` `PartOrdEmb.str` `RelIso.toRelEmbedding` `Preorder.toLE` `PartialOrder.toPreorder` `OrderIso.symm`	—	—

PartOrdEmb.Limits

Definitions

Name	Category	Theorems
`CoconePt` 📖	CompOp	3 math math: `cocone_pt_coe`, `CoconePt.fac_apply`, `cocone_ι_app`
`cocone` 📖	CompOp	2 math math: `cocone_pt_coe`, `cocone_ι_app`
`instPartialOrderCoconePt` 📖	CompOp	2 math math: `CoconePt.fac_apply`, `cocone_ι_app`
`isColimitCocone` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cocone_pt_coe` 📖	mathematical	—	`PartOrdEmb.carrier` `CategoryTheory.Limits.Cocone.pt` `PartOrdEmb` `PartOrdEmb.instCategory` `cocone` `CoconePt`	—	—
`cocone_ι_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `PartOrdEmb` `PartOrdEmb.instCategory` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `PartOrdEmb.of` `CoconePt` `instPartialOrderCoconePt` `CategoryTheory.Limits.Cocone.ι` `cocone` `PartOrdEmb.ofHom` `PartOrdEmb.carrier` `PartOrdEmb.str` `Preorder.toLE` `PartialOrder.toPreorder` `CategoryTheory.types` `CategoryTheory.Functor.comp` `CategoryTheory.forget` `OrderEmbedding` `instFunLikeOrderEmbedding` `PartOrdEmb.instConcreteCategoryOrderEmbeddingCarrier` `CategoryTheory.Limits.Cocone.pt`	—	—
`instHasColimit` 📖	mathematical	—	`CategoryTheory.Limits.HasColimit` `PartOrdEmb` `PartOrdEmb.instCategory`	—	`CategoryTheory.Limits.Types.hasColimit` `UnivLE.small` `UnivLE.self`
`instHasColimitsOfShape` 📖	mathematical	—	`CategoryTheory.Limits.HasColimitsOfShape` `PartOrdEmb` `PartOrdEmb.instCategory`	—	`instHasColimit`
`instHasFilteredColimitsOfSize` 📖	mathematical	—	`CategoryTheory.Limits.HasFilteredColimitsOfSize` `PartOrdEmb` `PartOrdEmb.instCategory`	—	`instHasColimitsOfShape`
`instPreservesColimitForgetOrderEmbeddingCarrier` 📖	mathematical	—	`CategoryTheory.Limits.PreservesColimit` `PartOrdEmb` `PartOrdEmb.instCategory` `CategoryTheory.types` `CategoryTheory.forget` `OrderEmbedding` `PartOrdEmb.carrier` `Preorder.toLE` `PartialOrder.toPreorder` `PartOrdEmb.str` `instFunLikeOrderEmbedding` `PartOrdEmb.instConcreteCategoryOrderEmbeddingCarrier`	—	`CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone` `CategoryTheory.Limits.Types.hasColimit` `UnivLE.small` `UnivLE.self`
`instPreservesColimitsOfShapeForgetOrderEmbeddingCarrier` 📖	mathematical	—	`CategoryTheory.Limits.PreservesColimitsOfShape` `PartOrdEmb` `PartOrdEmb.instCategory` `CategoryTheory.types` `CategoryTheory.forget` `OrderEmbedding` `PartOrdEmb.carrier` `Preorder.toLE` `PartialOrder.toPreorder` `PartOrdEmb.str` `instFunLikeOrderEmbedding` `PartOrdEmb.instConcreteCategoryOrderEmbeddingCarrier`	—	`instPreservesColimitForgetOrderEmbeddingCarrier`
`instPreservesFilteredColimitsOfSizeForgetOrderEmbeddingCarrier` 📖	mathematical	—	`CategoryTheory.Limits.PreservesFilteredColimitsOfSize` `PartOrdEmb` `PartOrdEmb.instCategory` `CategoryTheory.types` `CategoryTheory.forget` `OrderEmbedding` `PartOrdEmb.carrier` `Preorder.toLE` `PartialOrder.toPreorder` `PartOrdEmb.str` `instFunLikeOrderEmbedding` `PartOrdEmb.instConcreteCategoryOrderEmbeddingCarrier`	—	`instPreservesColimitsOfShapeForgetOrderEmbeddingCarrier`

PartOrdEmb.Limits.CoconePt

Definitions

Name	Category	Theorems
`desc` 📖	CompOp	1 math math: `fac_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fac_apply` 📖	mathematical	—	`DFunLike.coe` `OrderEmbedding` `PartOrdEmb.Limits.CoconePt` `PartOrdEmb.carrier` `CategoryTheory.Limits.Cocone.pt` `PartOrdEmb` `PartOrdEmb.instCategory` `Preorder.toLE` `PartialOrder.toPreorder` `PartOrdEmb.Limits.instPartialOrderCoconePt` `PartOrdEmb.str` `instFunLikeOrderEmbedding` `desc` `CategoryTheory.NatTrans.app` `CategoryTheory.types` `CategoryTheory.Functor.comp` `CategoryTheory.forget` `PartOrdEmb.instConcreteCategoryOrderEmbeddingCarrier` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cocone.ι` `CategoryTheory.ConcreteCategory.hom`	—	`CategoryTheory.Limits.IsColimit.fac`

(root)

Definitions

Name	Category	Theorems
`PartOrdEmb` 📖	CompData	30 math math: `PartOrdEmb.Limits.cocone_pt_coe`, `PartOrdEmb.comp_apply`, `PartOrdEmb.hom_inv_apply`, `PartOrdEmb.hom_comp`, `PartOrdEmb.Limits.CoconePt.fac_apply`, `PartOrdEmb.ofHom_apply`, `PartOrdEmb.Limits.cocone_ι_app`, `PartOrdEmb.Limits.instHasColimit`, `PartOrdEmb.dual_map`, `PartOrdEmb.hom_id`, `PartOrdEmb.ofHom_id`, `partOrdEmb_dual_comp_forget_to_pardOrd`, `PartOrdEmb.dualEquiv_inverse`, `PartOrdEmb.coe_comp`, `PartOrdEmb.inv_hom_apply`, `PartOrdEmb.id_apply`, `PartOrdEmb.forget_map`, `PartOrdEmb.Limits.instPreservesColimitsOfShapeForgetOrderEmbeddingCarrier`, `PartOrdEmb.Hom.injective`, `PartOrdEmb.ofHom_comp`, `PartOrdEmb.Hom.le_iff_le`, `PartOrdEmb.Limits.instHasColimitsOfShape`, `PartOrdEmb.Iso.mk_hom`, `PartOrdEmb.dualEquiv_functor`, `PartOrdEmb.Limits.instPreservesFilteredColimitsOfSizeForgetOrderEmbeddingCarrier`, `PartOrdEmb.ext_iff`, `PartOrdEmb.Limits.instPreservesColimitForgetOrderEmbeddingCarrier`, `PartOrdEmb.Limits.instHasFilteredColimitsOfSize`, `PartOrdEmb.coe_id`, `PartOrdEmb.Iso.mk_inv`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`partOrdEmb_dual_comp_forget_to_pardOrd` 📖	mathematical	—	`CategoryTheory.Functor.comp` `PartOrdEmb` `PartOrdEmb.instCategory` `PartOrd` `PartOrd.instCategory` `PartOrdEmb.dual` `CategoryTheory.forget₂` `OrderEmbedding` `PartOrdEmb.carrier` `Preorder.toLE` `PartialOrder.toPreorder` `PartOrdEmb.str` `instFunLikeOrderEmbedding` `PartOrdEmb.instConcreteCategoryOrderEmbeddingCarrier` `OrderHom` `PartOrd.carrier` `PartOrd.str` `OrderHom.instFunLike` `PartOrd.instConcreteCategoryOrderHomCarrier` `PartOrdEmb.hasForgetToPartOrd` `PartOrd.dual`	—	—

---

← Back to Index