Basic

📁 Source: Mathlib/CategoryTheory/Sigma/Basic.lean

Statistics

Metric	Count
Definitions `sigma`, `SigmaHom`, `comp`, `id`, `instCategoryStructSigma`, `instInhabited`, `desc`, `descMap`, `descUniq`, `incl`, `inclCompMap`, `inclDesc`, `map`, `mapComp`, `mapId`, `natIso`, `natTrans`, `sigma`, `sigma`	19
Theorems `assoc`, `comp_def`, `comp_id`, `id_comp`, `descUniq_hom_app`, `descUniq_inv_app`, `desc_map_mk`, `desc_obj`, `inclCompMap_hom_app`, `inclCompMap_inv_app`, `inclDesc_hom_app`, `inclDesc_inv_app`, `incl_map`, `incl_obj`, `instFaithfulSigmaIncl`, `instFullSigmaIncl`, `mapComp_hom_app`, `mapComp_inv_app`, `mapId_hom_app`, `mapId_inv_app`, `map_map`, `map_obj`, `natIso_hom`, `natIso_inv`, `natTrans_app`	25
Total	44

CategoryTheory.Sigma

Definitions

Name	Category	Theorems
`SigmaHom` 📖	CompData	—
`desc` 📖	CompOp	8 math math: `desc_map_mk`, `mapComp_hom_app`, `mapComp_inv_app`, `desc_obj`, `descUniq_inv_app`, `descUniq_hom_app`, `inclDesc_hom_app`, `inclDesc_inv_app`
`descMap` 📖	CompOp	1 math math: `CategoryTheory.decomposedTo_map`
`descUniq` 📖	CompOp	2 math math: `descUniq_inv_app`, `descUniq_hom_app`
`incl` 📖	CompOp	15 math math: `incl_map`, `mapComp_hom_app`, `mapComp_inv_app`, `natIso_inv`, `natTrans_app`, `descUniq_inv_app`, `instFullSigmaIncl`, `inclCompMap_hom_app`, `instFaithfulSigmaIncl`, `inclCompMap_inv_app`, `incl_obj`, `descUniq_hom_app`, `natIso_hom`, `inclDesc_hom_app`, `inclDesc_inv_app`
`inclCompMap` 📖	CompOp	2 math math: `inclCompMap_hom_app`, `inclCompMap_inv_app`
`inclDesc` 📖	CompOp	2 math math: `inclDesc_hom_app`, `inclDesc_inv_app`
`map` 📖	CompOp	8 math math: `mapComp_hom_app`, `mapComp_inv_app`, `inclCompMap_hom_app`, `inclCompMap_inv_app`, `mapId_hom_app`, `mapId_inv_app`, `map_obj`, `map_map`
`mapComp` 📖	CompOp	2 math math: `mapComp_hom_app`, `mapComp_inv_app`
`mapId` 📖	CompOp	2 math math: `mapId_hom_app`, `mapId_inv_app`
`natIso` 📖	CompOp	2 math math: `natIso_inv`, `natIso_hom`
`natTrans` 📖	CompOp	3 math math: `natIso_inv`, `natTrans_app`, `natIso_hom`
`sigma` 📖	CompOp	29 math math: `incl_map`, `desc_map_mk`, `mapComp_hom_app`, `mapComp_inv_app`, `CategoryTheory.instFaithfulDecomposedDecomposedTo`, `CategoryTheory.instFullDecomposedDecomposedTo`, `CategoryTheory.decomposedEquiv_functor`, `natIso_inv`, `desc_obj`, `natTrans_app`, `CategoryTheory.decomposedTo_map`, `descUniq_inv_app`, `CategoryTheory.instEssSurjDecomposedDecomposedTo`, `instFullSigmaIncl`, `CategoryTheory.instIsEquivalenceDecomposedDecomposedTo`, `inclCompMap_hom_app`, `instFaithfulSigmaIncl`, `inclCompMap_inv_app`, `mapId_hom_app`, `incl_obj`, `mapId_inv_app`, `CategoryTheory.inclusion_comp_decomposedTo`, `descUniq_hom_app`, `CategoryTheory.decomposedTo_obj`, `map_obj`, `map_map`, `natIso_hom`, `inclDesc_hom_app`, `inclDesc_inv_app`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`descUniq_hom_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `sigma` `desc` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `descUniq` `CategoryTheory.Functor.comp` `incl`	—	—
`descUniq_inv_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `sigma` `desc` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `descUniq` `CategoryTheory.Functor.comp` `incl`	—	—
`desc_map_mk` 📖	mathematical	—	`CategoryTheory.Functor.map` `sigma` `desc`	—	—
`desc_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `sigma` `desc`	—	—
`inclCompMap_hom_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `sigma` `CategoryTheory.Functor.comp` `incl` `map` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `inclCompMap` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	—
`inclCompMap_inv_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `sigma` `CategoryTheory.Functor.comp` `incl` `map` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `inclCompMap` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	—
`inclDesc_hom_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `sigma` `incl` `desc` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `inclDesc` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj`	—	—
`inclDesc_inv_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `sigma` `incl` `desc` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `inclDesc` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj`	—	—
`incl_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `sigma` `incl`	—	—
`incl_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `sigma` `incl`	—	—
`instFaithfulSigmaIncl` 📖	mathematical	—	`CategoryTheory.Functor.Faithful` `sigma` `incl`	—	—
`instFullSigmaIncl` 📖	mathematical	—	`CategoryTheory.Functor.Full` `sigma` `incl`	—	—
`mapComp_hom_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `sigma` `CategoryTheory.Functor.comp` `map` `desc` `incl` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `mapComp` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	`CategoryTheory.Functor.map_id` `CategoryTheory.Category.comp_id`
`mapComp_inv_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `sigma` `desc` `incl` `CategoryTheory.Functor.comp` `map` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `mapComp` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	`CategoryTheory.Functor.map_id` `CategoryTheory.Category.comp_id`
`mapId_hom_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `sigma` `map` `CategoryTheory.Functor.id` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `mapId` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	—
`mapId_inv_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `sigma` `CategoryTheory.Functor.id` `map` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `mapId` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	—
`map_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `sigma` `map`	—	—
`map_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `sigma` `map`	—	—
`natIso_hom` 📖	mathematical	—	`CategoryTheory.Iso.hom` `CategoryTheory.Functor` `sigma` `CategoryTheory.Functor.category` `natIso` `natTrans` `CategoryTheory.Functor.comp` `incl`	—	—
`natIso_inv` 📖	mathematical	—	`CategoryTheory.Iso.inv` `CategoryTheory.Functor` `sigma` `CategoryTheory.Functor.category` `natIso` `natTrans` `CategoryTheory.Functor.comp` `incl`	—	—
`natTrans_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `sigma` `natTrans` `CategoryTheory.Functor.comp` `incl`	—	—

CategoryTheory.Sigma.Functor

Definitions

Name	Category	Theorems
`sigma` 📖	CompOp	—

CategoryTheory.Sigma.SigmaHom

Definitions

Name	Category	Theorems
`comp` 📖	CompOp	1 math math: `comp_def`
`id` 📖	CompOp	—
`instCategoryStructSigma` 📖	CompOp	3 math math: `id_comp`, `assoc`, `comp_id`
`instInhabited` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `instCategoryStructSigma`	—	`CategoryTheory.Category.assoc`
`comp_def` 📖	mathematical	—	`comp` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	—	—
`comp_id` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `instCategoryStructSigma` `CategoryTheory.CategoryStruct.id`	—	`CategoryTheory.Category.comp_id`
`id_comp` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `instCategoryStructSigma` `CategoryTheory.CategoryStruct.id`	—	`CategoryTheory.Category.id_comp`

CategoryTheory.Sigma.natTrans

Definitions

Name	Category	Theorems
`sigma` 📖	CompOp	—

---

← Back to Index