Equalizer

📁 Source: Mathlib/CategoryTheory/Subfunctor/Equalizer.lean

Statistics

Metric	Count
Definitions equalizer, fork, forkIsLimit, ι, equalizer, fork, forkIsLimit, ι	8
Theorems condition, fork_ι, lift_ι, lift_ι', ι_ι, equalizer_eq_iff, equalizer_le, equalizer_self, mem_equalizer_iff, range_le_equalizer_iff, condition, condition_assoc, fork_pt, fork_ι, lift_ι, lift_ι', lift_ι'_assoc, lift_ι_assoc, ι_ι, ι_ι_assoc, equalizer_eq_iff, equalizer_le, equalizer_obj, equalizer_self, instMonoFunctorTypeι_1, mem_equalizer_iff, range_le_equalizer_iff	27
Total	35

CategoryTheory.Subfunctor

Definitions

Name	Category	Theorems
equalizer 📖	CompOp	25 math math: Subpresheaf.equalizer_le, Subpresheaf.equalizer.condition, range_le_equalizer_iff, equalizer_self, equalizer.lift_ι', equalizer_eq_iff, equalizer.ι_ι_assoc, equalizer.lift_ι'_assoc, Subpresheaf.mem_equalizer_iff, equalizer_le, Subpresheaf.range_le_equalizer_iff, mem_equalizer_iff, Subpresheaf.equalizer_eq_iff, equalizer.condition, equalizer.lift_ι, instMonoFunctorTypeι_1, equalizer.fork_pt, equalizer.lift_ι_assoc, Subpresheaf.equalizer_self, Subpresheaf.equalizer.ι_ι, Subpresheaf.equalizer.lift_ι, equalizer.condition_assoc, equalizer_obj, equalizer.ι_ι, Subpresheaf.equalizer.lift_ι'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equalizer_eq_iff 📖	mathematical	—	equalizer	—	range_le_equalizer_iff CategoryTheory.Category.id_comp range_ι le_refl le_antisymm equalizer_le
equalizer_le 📖	mathematical	—	CategoryTheory.Subfunctor Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubfunctor equalizer	—	—
equalizer_obj 📖	mathematical	—	obj equalizer setOf CategoryTheory.Functor.obj CategoryTheory.types Set Set.instMembership CategoryTheory.NatTrans.app toFunctor	—	—
equalizer_self 📖	mathematical	—	equalizer	—	ext Set.ext
instMonoFunctorTypeι_1 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category toFunctor equalizer equalizer.ι	—	equalizer_le instMonoFunctorTypeHomOfLe
mem_equalizer_iff 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.types Set Set.instMembership obj equalizer CategoryTheory.NatTrans.app toFunctor	—	Subtype.coe_eta
range_le_equalizer_iff 📖	mathematical	—	CategoryTheory.Subfunctor Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubfunctor range CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category toFunctor ι equalizer	—	CategoryTheory.NatTrans.ext_iff Subtype.coe_eta

CategoryTheory.Subfunctor.Subpresheaf

Definitions

Name	Category	Theorems
equalizer 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equalizer_eq_iff 📖	mathematical	—	CategoryTheory.Subfunctor.equalizer	—	CategoryTheory.Subfunctor.equalizer_eq_iff
equalizer_le 📖	mathematical	—	CategoryTheory.Subfunctor Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubfunctor CategoryTheory.Subfunctor.equalizer	—	CategoryTheory.Subfunctor.equalizer_le
equalizer_self 📖	mathematical	—	CategoryTheory.Subfunctor.equalizer	—	CategoryTheory.Subfunctor.equalizer_self
mem_equalizer_iff 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.types Set Set.instMembership CategoryTheory.Subfunctor.obj CategoryTheory.Subfunctor.equalizer CategoryTheory.NatTrans.app CategoryTheory.Subfunctor.toFunctor	—	CategoryTheory.Subfunctor.mem_equalizer_iff
range_le_equalizer_iff 📖	mathematical	—	CategoryTheory.Subfunctor Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubfunctor CategoryTheory.Subfunctor.range CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Subfunctor.toFunctor CategoryTheory.Subfunctor.ι CategoryTheory.Subfunctor.equalizer	—	CategoryTheory.Subfunctor.range_le_equalizer_iff

CategoryTheory.Subfunctor.Subpresheaf.equalizer

Definitions

Name	Category	Theorems
fork 📖	CompOp	—
forkIsLimit 📖	CompOp	—
ι 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
condition 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Subfunctor.toFunctor CategoryTheory.Subfunctor.equalizer CategoryTheory.Subfunctor.equalizer.ι	—	CategoryTheory.Subfunctor.equalizer.condition
fork_ι 📖	mathematical	—	CategoryTheory.Limits.Fork.ι CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.Subfunctor.toFunctor CategoryTheory.Subfunctor.equalizer.fork CategoryTheory.Subfunctor.equalizer.ι	—	CategoryTheory.Subfunctor.equalizer.fork_ι
lift_ι 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Subfunctor.toFunctor	CategoryTheory.Subfunctor.equalizer CategoryTheory.Subfunctor.equalizer.lift CategoryTheory.Subfunctor.equalizer.ι	—	CategoryTheory.Subfunctor.equalizer.lift_ι
lift_ι' 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Subfunctor.toFunctor	CategoryTheory.Subfunctor.equalizer CategoryTheory.Subfunctor.equalizer.lift CategoryTheory.Subfunctor.ι	—	CategoryTheory.Subfunctor.equalizer.lift_ι'
ι_ι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Subfunctor.toFunctor CategoryTheory.Subfunctor.equalizer CategoryTheory.Subfunctor.equalizer.ι CategoryTheory.Subfunctor.ι	—	CategoryTheory.Subfunctor.equalizer.ι_ι

CategoryTheory.Subfunctor.equalizer

Definitions

Name	Category	Theorems
fork 📖	CompOp	3 math math: CategoryTheory.Subfunctor.Subpresheaf.equalizer.fork_ι, fork_pt, fork_ι
forkIsLimit 📖	CompOp	—
ι 📖	CompOp	12 math math: CategoryTheory.Subfunctor.Subpresheaf.equalizer.fork_ι, CategoryTheory.Subfunctor.Subpresheaf.equalizer.condition, ι_ι_assoc, condition, lift_ι, CategoryTheory.Subfunctor.instMonoFunctorTypeι_1, lift_ι_assoc, CategoryTheory.Subfunctor.Subpresheaf.equalizer.ι_ι, CategoryTheory.Subfunctor.Subpresheaf.equalizer.lift_ι, condition_assoc, ι_ι, fork_ι

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
condition 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Subfunctor.toFunctor CategoryTheory.Subfunctor.equalizer ι	—	CategoryTheory.Subfunctor.range_ι
condition_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Subfunctor.toFunctor CategoryTheory.Subfunctor.equalizer ι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' condition
fork_pt 📖	mathematical	—	CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.Limits.parallelPair CategoryTheory.Subfunctor.toFunctor fork CategoryTheory.Subfunctor.equalizer	—	—
fork_ι 📖	mathematical	—	CategoryTheory.Limits.Fork.ι CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.Subfunctor.toFunctor fork ι	—	—
lift_ι 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Subfunctor.toFunctor	CategoryTheory.Subfunctor.equalizer lift ι	—	—
lift_ι' 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Subfunctor.toFunctor	CategoryTheory.Subfunctor.equalizer lift CategoryTheory.Subfunctor.ι	—	—
lift_ι'_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Subfunctor.toFunctor	CategoryTheory.Subfunctor.equalizer lift CategoryTheory.Subfunctor.ι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_ι'
lift_ι_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Subfunctor.toFunctor	CategoryTheory.Subfunctor.equalizer lift ι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_ι
ι_ι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Subfunctor.toFunctor CategoryTheory.Subfunctor.equalizer ι CategoryTheory.Subfunctor.ι	—	—
ι_ι_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Subfunctor.toFunctor CategoryTheory.Subfunctor.equalizer ι CategoryTheory.Subfunctor.ι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_ι

---

← Back to Index