Elementwise

📁 Source: Mathlib/CategoryTheory/ConcreteCategory/Elementwise.lean

Statistics

Metric	Count
Definitions	0
Theorems w_apply, w_apply, condition_apply, π_desc_apply, w_apply, ι_desc_apply, condition_apply, lift_ι_apply, lift_π_apply, w_apply	10
Total	10

CategoryTheory.Limits.Cocone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
w_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj pt CategoryTheory.ConcreteCategory.hom CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const ι CategoryTheory.Functor.map	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise w

CategoryTheory.Limits.Cone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
w_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj CategoryTheory.ConcreteCategory.hom CategoryTheory.Functor.map pt CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const π	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise w

CategoryTheory.Limits.cokernel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
condition_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.Limits.cokernel CategoryTheory.ConcreteCategory.hom π Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise condition
π_desc_apply 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	DFunLike.coe CategoryTheory.Limits.cokernel CategoryTheory.ConcreteCategory.hom desc π	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise π_desc

CategoryTheory.Limits.colimit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
w_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj CategoryTheory.Limits.colimit CategoryTheory.ConcreteCategory.hom ι CategoryTheory.Functor.map	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise w
ι_desc_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.Limits.colimit CategoryTheory.Limits.Cocone.pt CategoryTheory.ConcreteCategory.hom desc CategoryTheory.Functor.obj ι CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.ι	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise ι_desc

CategoryTheory.Limits.kernel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
condition_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.kernel ι Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise condition
lift_ι_apply 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	DFunLike.coe CategoryTheory.Limits.kernel CategoryTheory.ConcreteCategory.hom ι lift	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise lift_ι

CategoryTheory.Limits.limit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lift_π_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.Limits.limit CategoryTheory.Functor.obj CategoryTheory.ConcreteCategory.hom π CategoryTheory.Limits.Cone.pt lift CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.π	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise lift_π
w_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj CategoryTheory.ConcreteCategory.hom CategoryTheory.Functor.map CategoryTheory.Limits.limit π	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise w

---

← Back to Index