The equalizer of two morphisms of functors, as a subfunctor #

If F₁ and F₂ are type-valued functors, A : Subfunctor F₁, and f and g are two morphisms A.toFunctor ⟶ F₂, we introduce Subcomplex.equalizer f g, which is the subfunctor of F₁ contained in A where f and g coincide.

source

def CategoryTheory.Subfunctor.equalizer {C : Type u} [Category.{v, u} C] {F₁ F₂ : Functor C (Type w)} {A : Subfunctor F₁} (f g : A.toFunctor ⟶ F₂) :

Subfunctor F₁

The equalizer of two morphisms of type-valued functors of types of the form A.toFunctor ⟶ F₂ with A : Subfunctor F₁, as a subcomplex of F₁.

Equations

CategoryTheory.Subfunctor.equalizer f g = { obj := fun (U : C) => {x : F₁.obj U | ∃ (hx : x ∈ A.obj U), f.app U ⟨x, hx⟩ = g.app U ⟨x, hx⟩}, map := ⋯ }

Instances For

source

theorem CategoryTheory.Subfunctor.equalizer_obj {C : Type u} [Category.{v, u} C] {F₁ F₂ : Functor C (Type w)} {A : Subfunctor F₁} (f g : A.toFunctor ⟶ F₂) (U : C) :

(Subfunctor.equalizer f g).obj U = {x : F₁.obj U | ∃ (hx : x ∈ A.obj U), f.app U ⟨x, hx⟩ = g.app U ⟨x, hx⟩}

source

theorem CategoryTheory.Subfunctor.equalizer_le {C : Type u} [Category.{v, u} C] {F₁ F₂ : Functor C (Type w)} {A : Subfunctor F₁} (f g : A.toFunctor ⟶ F₂) :

Subfunctor.equalizer f g ≤ A

source

@[simp]

theorem CategoryTheory.Subfunctor.equalizer_self {C : Type u} [Category.{v, u} C] {F₁ F₂ : Functor C (Type w)} {A : Subfunctor F₁} (f : A.toFunctor ⟶ F₂) :

Subfunctor.equalizer f f = A

source

theorem CategoryTheory.Subfunctor.mem_equalizer_iff {C : Type u} [Category.{v, u} C] {F₁ F₂ : Functor C (Type w)} {A : Subfunctor F₁} (f g : A.toFunctor ⟶ F₂) {i : C} (x : A.toFunctor.obj i) :

↑x ∈ (Subfunctor.equalizer f g).obj i ↔ f.app i x = g.app i x

source

theorem CategoryTheory.Subfunctor.range_le_equalizer_iff {C : Type u} [Category.{v, u} C] {F₁ F₂ : Functor C (Type w)} {A : Subfunctor F₁} (f g : A.toFunctor ⟶ F₂) {G : Functor C (Type w)} (φ : G ⟶ A.toFunctor) :

range (CategoryStruct.comp φ A.ι) ≤ Subfunctor.equalizer f g ↔ CategoryStruct.comp φ f = CategoryStruct.comp φ g

source

theorem CategoryTheory.Subfunctor.equalizer_eq_iff {C : Type u} [Category.{v, u} C] {F₁ F₂ : Functor C (Type w)} {A : Subfunctor F₁} (f g : A.toFunctor ⟶ F₂) :

Subfunctor.equalizer f g = A ↔ f = g

source

def CategoryTheory.Subfunctor.equalizer.ι {C : Type u} [Category.{v, u} C] {F₁ F₂ : Functor C (Type w)} {A : Subfunctor F₁} (f g : A.toFunctor ⟶ F₂) :

(Subfunctor.equalizer f g).toFunctor ⟶ A.toFunctor

Given two morphisms f and g in A.toFunctor ⟶ F₂, this is the monomorphism of functors corresponding to the inclusion Subfunctor.equalizer f g ≤ A.

Equations

CategoryTheory.Subfunctor.equalizer.ι f g = CategoryTheory.Subfunctor.homOfLe ⋯

Instances For

source

instance CategoryTheory.Subfunctor.instMonoFunctorTypeι_1 {C : Type u} [Category.{v, u} C] {F₁ F₂ : Functor C (Type w)} {A : Subfunctor F₁} (f g : A.toFunctor ⟶ F₂) :

Mono (equalizer.ι f g)

source

@[simp]

theorem CategoryTheory.Subfunctor.equalizer.ι_ι {C : Type u} [Category.{v, u} C] {F₁ F₂ : Functor C (Type w)} {A : Subfunctor F₁} (f g : A.toFunctor ⟶ F₂) :

CategoryStruct.comp (ι f g) A.ι = (Subfunctor.equalizer f g).ι

source

@[simp]

theorem CategoryTheory.Subfunctor.equalizer.ι_ι_assoc {C : Type u} [Category.{v, u} C] {F₁ F₂ : Functor C (Type w)} {A : Subfunctor F₁} (f g : A.toFunctor ⟶ F₂) {Z : Functor C (Type w)} (h : F₁ ⟶ Z) :

CategoryStruct.comp (ι f g) (CategoryStruct.comp A.ι h) = CategoryStruct.comp (Subfunctor.equalizer f g).ι h

source

theorem CategoryTheory.Subfunctor.equalizer.condition {C : Type u} [Category.{v, u} C] {F₁ F₂ : Functor C (Type w)} {A : Subfunctor F₁} (f g : A.toFunctor ⟶ F₂) :

CategoryStruct.comp (ι f g) f = CategoryStruct.comp (ι f g) g

source

theorem CategoryTheory.Subfunctor.equalizer.condition_assoc {C : Type u} [Category.{v, u} C] {F₁ F₂ : Functor C (Type w)} {A : Subfunctor F₁} (f g : A.toFunctor ⟶ F₂) {Z : Functor C (Type w)} (h : F₂ ⟶ Z) :

CategoryStruct.comp (ι f g) (CategoryStruct.comp f h) = CategoryStruct.comp (ι f g) (CategoryStruct.comp g h)

source

def CategoryTheory.Subfunctor.equalizer.lift {C : Type u} [Category.{v, u} C] {F₁ F₂ : Functor C (Type w)} {A : Subfunctor F₁} (f g : A.toFunctor ⟶ F₂) {G : Functor C (Type w)} (φ : G ⟶ A.toFunctor) (w : CategoryStruct.comp φ f = CategoryStruct.comp φ g) :

G ⟶ (Subfunctor.equalizer f g).toFunctor

Given two morphisms f and g in A.toFunctor ⟶ F₂, if φ : G ⟶ A.toFunctor is such that φ ≫ f = φ ≫ g, then this is the lifted morphism G ⟶ (Subfunctor.equalizer f g).toFunctor. This is part of the universal property of the equalizer that is satisfied by the functor (Subfunctor.equalizer f g).toFunctor.

Equations

CategoryTheory.Subfunctor.equalizer.lift f g φ w = CategoryTheory.Subfunctor.lift (CategoryTheory.CategoryStruct.comp φ A.ι) ⋯

Instances For

source

@[simp]

theorem CategoryTheory.Subfunctor.equalizer.lift_ι' {C : Type u} [Category.{v, u} C] {F₁ F₂ : Functor C (Type w)} {A : Subfunctor F₁} (f g : A.toFunctor ⟶ F₂) {G : Functor C (Type w)} (φ : G ⟶ A.toFunctor) (w : CategoryStruct.comp φ f = CategoryStruct.comp φ g) :

CategoryStruct.comp (lift f g φ w) (Subfunctor.equalizer f g).ι = CategoryStruct.comp φ A.ι

source

@[simp]

theorem CategoryTheory.Subfunctor.equalizer.lift_ι'_assoc {C : Type u} [Category.{v, u} C] {F₁ F₂ : Functor C (Type w)} {A : Subfunctor F₁} (f g : A.toFunctor ⟶ F₂) {G : Functor C (Type w)} (φ : G ⟶ A.toFunctor) (w : CategoryStruct.comp φ f = CategoryStruct.comp φ g) {Z : Functor C (Type w)} (h : F₁ ⟶ Z) :

CategoryStruct.comp (lift f g φ w) (CategoryStruct.comp (Subfunctor.equalizer f g).ι h) = CategoryStruct.comp φ (CategoryStruct.comp A.ι h)

source

@[simp]

theorem CategoryTheory.Subfunctor.equalizer.lift_ι {C : Type u} [Category.{v, u} C] {F₁ F₂ : Functor C (Type w)} {A : Subfunctor F₁} (f g : A.toFunctor ⟶ F₂) {G : Functor C (Type w)} (φ : G ⟶ A.toFunctor) (w : CategoryStruct.comp φ f = CategoryStruct.comp φ g) :

CategoryStruct.comp (lift f g φ w) (ι f g) = φ

source

@[simp]

theorem CategoryTheory.Subfunctor.equalizer.lift_ι_assoc {C : Type u} [Category.{v, u} C] {F₁ F₂ : Functor C (Type w)} {A : Subfunctor F₁} (f g : A.toFunctor ⟶ F₂) {G : Functor C (Type w)} (φ : G ⟶ A.toFunctor) (w : CategoryStruct.comp φ f = CategoryStruct.comp φ g) {Z : Functor C (Type w)} (h : A.toFunctor ⟶ Z) :

CategoryStruct.comp (lift f g φ w) (CategoryStruct.comp (ι f g) h) = CategoryStruct.comp φ h

source

def CategoryTheory.Subfunctor.equalizer.fork {C : Type u} [Category.{v, u} C] {F₁ F₂ : Functor C (Type w)} {A : Subfunctor F₁} (f g : A.toFunctor ⟶ F₂) :

Limits.Fork f g

The (limit) fork which expresses (Subfunctor.equalizer f g).toFunctor as the equalizer of f and g.

Equations

CategoryTheory.Subfunctor.equalizer.fork f g = CategoryTheory.Limits.Fork.ofι (CategoryTheory.Subfunctor.equalizer.ι f g) ⋯

Instances For

source

@[simp]

theorem CategoryTheory.Subfunctor.equalizer.fork_pt {C : Type u} [Category.{v, u} C] {F₁ F₂ : Functor C (Type w)} {A : Subfunctor F₁} (f g : A.toFunctor ⟶ F₂) :

(fork f g).pt = (Subfunctor.equalizer f g).toFunctor

source

@[simp]

theorem CategoryTheory.Subfunctor.equalizer.fork_ι {C : Type u} [Category.{v, u} C] {F₁ F₂ : Functor C (Type w)} {A : Subfunctor F₁} (f g : A.toFunctor ⟶ F₂) :

(fork f g).ι = ι f g

source

def CategoryTheory.Subfunctor.equalizer.forkIsLimit {C : Type u} [Category.{v, u} C] {F₁ F₂ : Functor C (Type w)} {A : Subfunctor F₁} (f g : A.toFunctor ⟶ F₂) :

Limits.IsLimit (fork f g)

(Subfunctor.equalizer f g).toFunctor is the equalizer of f and g.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[deprecated CategoryTheory.Subfunctor.equalizer (since := "2025-12-11")]

def CategoryTheory.Subfunctor.Subpresheaf.equalizer {C : Type u} [Category.{v, u} C] {F₁ F₂ : Functor C (Type w)} {A : Subfunctor F₁} (f g : A.toFunctor ⟶ F₂) :

Subfunctor F₁

Alias of CategoryTheory.Subfunctor.equalizer.

The equalizer of two morphisms of type-valued functors of types of the form A.toFunctor ⟶ F₂ with A : Subfunctor F₁, as a subcomplex of F₁.

Equations

@CategoryTheory.Subfunctor.Subpresheaf.equalizer = @CategoryTheory.Subfunctor.equalizer

Instances For

source

@[deprecated CategoryTheory.Subfunctor.equalizer_le (since := "2025-12-11")]

theorem CategoryTheory.Subfunctor.Subpresheaf.equalizer_le {C : Type u} [Category.{v, u} C] {F₁ F₂ : Functor C (Type w)} {A : Subfunctor F₁} (f g : A.toFunctor ⟶ F₂) :

Subfunctor.equalizer f g ≤ A

Alias of CategoryTheory.Subfunctor.equalizer_le.

source

@[deprecated CategoryTheory.Subfunctor.equalizer_self (since := "2025-12-11")]

theorem CategoryTheory.Subfunctor.Subpresheaf.equalizer_self {C : Type u} [Category.{v, u} C] {F₁ F₂ : Functor C (Type w)} {A : Subfunctor F₁} (f : A.toFunctor ⟶ F₂) :

Subfunctor.equalizer f f = A

Alias of CategoryTheory.Subfunctor.equalizer_self.

source

@[deprecated CategoryTheory.Subfunctor.mem_equalizer_iff (since := "2025-12-11")]

theorem CategoryTheory.Subfunctor.Subpresheaf.mem_equalizer_iff {C : Type u} [Category.{v, u} C] {F₁ F₂ : Functor C (Type w)} {A : Subfunctor F₁} (f g : A.toFunctor ⟶ F₂) {i : C} (x : A.toFunctor.obj i) :

↑x ∈ (Subfunctor.equalizer f g).obj i ↔ f.app i x = g.app i x

Alias of CategoryTheory.Subfunctor.mem_equalizer_iff.

source

@[deprecated CategoryTheory.Subfunctor.range_le_equalizer_iff (since := "2025-12-11")]

theorem CategoryTheory.Subfunctor.Subpresheaf.range_le_equalizer_iff {C : Type u} [Category.{v, u} C] {F₁ F₂ : Functor C (Type w)} {A : Subfunctor F₁} (f g : A.toFunctor ⟶ F₂) {G : Functor C (Type w)} (φ : G ⟶ A.toFunctor) :

Subfunctor.range (CategoryStruct.comp φ A.ι) ≤ Subfunctor.equalizer f g ↔ CategoryStruct.comp φ f = CategoryStruct.comp φ g

Alias of CategoryTheory.Subfunctor.range_le_equalizer_iff.

source

@[deprecated CategoryTheory.Subfunctor.equalizer_eq_iff (since := "2025-12-11")]

theorem CategoryTheory.Subfunctor.Subpresheaf.equalizer_eq_iff {C : Type u} [Category.{v, u} C] {F₁ F₂ : Functor C (Type w)} {A : Subfunctor F₁} (f g : A.toFunctor ⟶ F₂) :

Subfunctor.equalizer f g = A ↔ f = g

Alias of CategoryTheory.Subfunctor.equalizer_eq_iff.

source

@[deprecated CategoryTheory.Subfunctor.equalizer.ι (since := "2025-12-11")]

def CategoryTheory.Subfunctor.Subpresheaf.equalizer.ι {C : Type u} [Category.{v, u} C] {F₁ F₂ : Functor C (Type w)} {A : Subfunctor F₁} (f g : A.toFunctor ⟶ F₂) :

(Subfunctor.equalizer f g).toFunctor ⟶ A.toFunctor

Alias of CategoryTheory.Subfunctor.equalizer.ι.

Given two morphisms f and g in A.toFunctor ⟶ F₂, this is the monomorphism of functors corresponding to the inclusion Subfunctor.equalizer f g ≤ A.

Equations

@CategoryTheory.Subfunctor.Subpresheaf.equalizer.ι = @CategoryTheory.Subfunctor.equalizer.ι

Instances For

source

@[deprecated CategoryTheory.Subfunctor.equalizer.ι_ι (since := "2025-12-11")]

theorem CategoryTheory.Subfunctor.Subpresheaf.equalizer.ι_ι {C : Type u} [Category.{v, u} C] {F₁ F₂ : Functor C (Type w)} {A : Subfunctor F₁} (f g : A.toFunctor ⟶ F₂) :

CategoryStruct.comp (Subfunctor.equalizer.ι f g) A.ι = (Subfunctor.equalizer f g).ι

Alias of CategoryTheory.Subfunctor.equalizer.ι_ι.

source

@[deprecated CategoryTheory.Subfunctor.equalizer.condition (since := "2025-12-11")]

theorem CategoryTheory.Subfunctor.Subpresheaf.equalizer.condition {C : Type u} [Category.{v, u} C] {F₁ F₂ : Functor C (Type w)} {A : Subfunctor F₁} (f g : A.toFunctor ⟶ F₂) :

CategoryStruct.comp (Subfunctor.equalizer.ι f g) f = CategoryStruct.comp (Subfunctor.equalizer.ι f g) g

Alias of CategoryTheory.Subfunctor.equalizer.condition.

source

@[deprecated CategoryTheory.Subfunctor.equalizer.lift (since := "2025-12-11")]

def CategoryTheory.Subfunctor.Subpresheaf.equalizer.lift {C : Type u} [Category.{v, u} C] {F₁ F₂ : Functor C (Type w)} {A : Subfunctor F₁} (f g : A.toFunctor ⟶ F₂) {G : Functor C (Type w)} (φ : G ⟶ A.toFunctor) (w : CategoryStruct.comp φ f = CategoryStruct.comp φ g) :

G ⟶ (Subfunctor.equalizer f g).toFunctor

Alias of CategoryTheory.Subfunctor.equalizer.lift.

Equations

@CategoryTheory.Subfunctor.Subpresheaf.equalizer.lift = @CategoryTheory.Subfunctor.equalizer.lift

Instances For

source

@[deprecated CategoryTheory.Subfunctor.equalizer.lift_ι' (since := "2025-12-11")]

theorem CategoryTheory.Subfunctor.Subpresheaf.equalizer.lift_ι' {C : Type u} [Category.{v, u} C] {F₁ F₂ : Functor C (Type w)} {A : Subfunctor F₁} (f g : A.toFunctor ⟶ F₂) {G : Functor C (Type w)} (φ : G ⟶ A.toFunctor) (w : CategoryStruct.comp φ f = CategoryStruct.comp φ g) :

CategoryStruct.comp (Subfunctor.equalizer.lift f g φ w) (Subfunctor.equalizer f g).ι = CategoryStruct.comp φ A.ι

Alias of CategoryTheory.Subfunctor.equalizer.lift_ι'.

source

@[deprecated CategoryTheory.Subfunctor.equalizer.lift_ι (since := "2025-12-11")]

theorem CategoryTheory.Subfunctor.Subpresheaf.equalizer.lift_ι {C : Type u} [Category.{v, u} C] {F₁ F₂ : Functor C (Type w)} {A : Subfunctor F₁} (f g : A.toFunctor ⟶ F₂) {G : Functor C (Type w)} (φ : G ⟶ A.toFunctor) (w : CategoryStruct.comp φ f = CategoryStruct.comp φ g) :

CategoryStruct.comp (Subfunctor.equalizer.lift f g φ w) (Subfunctor.equalizer.ι f g) = φ

Alias of CategoryTheory.Subfunctor.equalizer.lift_ι.

source

@[deprecated CategoryTheory.Subfunctor.equalizer.fork (since := "2025-12-11")]

def CategoryTheory.Subfunctor.Subpresheaf.equalizer.fork {C : Type u} [Category.{v, u} C] {F₁ F₂ : Functor C (Type w)} {A : Subfunctor F₁} (f g : A.toFunctor ⟶ F₂) :

Limits.Fork f g

Alias of CategoryTheory.Subfunctor.equalizer.fork.

The (limit) fork which expresses (Subfunctor.equalizer f g).toFunctor as the equalizer of f and g.

Equations

@CategoryTheory.Subfunctor.Subpresheaf.equalizer.fork = @CategoryTheory.Subfunctor.equalizer.fork

Instances For

source

@[deprecated CategoryTheory.Subfunctor.equalizer.fork_ι (since := "2025-12-11")]

theorem CategoryTheory.Subfunctor.Subpresheaf.equalizer.fork_ι {C : Type u} [Category.{v, u} C] {F₁ F₂ : Functor C (Type w)} {A : Subfunctor F₁} (f g : A.toFunctor ⟶ F₂) :

(Subfunctor.equalizer.fork f g).ι = Subfunctor.equalizer.ι f g

Alias of CategoryTheory.Subfunctor.equalizer.fork_ι.

source

@[deprecated CategoryTheory.Subfunctor.equalizer.forkIsLimit (since := "2025-12-11")]

def CategoryTheory.Subfunctor.Subpresheaf.equalizer.forkIsLimit {C : Type u} [Category.{v, u} C] {F₁ F₂ : Functor C (Type w)} {A : Subfunctor F₁} (f g : A.toFunctor ⟶ F₂) :

Limits.IsLimit (Subfunctor.equalizer.fork f g)

Alias of CategoryTheory.Subfunctor.equalizer.forkIsLimit.

(Subfunctor.equalizer f g).toFunctor is the equalizer of f and g.

Equations

@CategoryTheory.Subfunctor.Subpresheaf.equalizer.forkIsLimit = @CategoryTheory.Subfunctor.equalizer.forkIsLimit

Instances For

Documentation

Mathlib.CategoryTheory.Subfunctor.Equalizer

The equalizer of two morphisms of functors, as a subfunctor #