The equalizer of two morphisms of presheaves, as a subpresheaf

If F₁ and F₂ are presheaves of types, A : Subpresheaf F₁, and f and g are two morphisms A.toPresheaf ⟶ F₂, we introduce Subcomplex.equalizer f g, which is the subpresheaf of F₁ contained in A where f and g coincide.

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

The equalizer of two morphisms of presheaves of types of the form A.toPresheaf ⟶ F₂ with A : Subpresheaf F₁, as a subcomplex of F₁.

theorem CategoryTheory.Subpresheaf.equalizer_obj {C : Type u} [Category.{v, u} C] {F₁ F₂ : Functor Cᵒᵖ (Type w)} {A : Subpresheaf F₁} (f g : A.toPresheaf ⟶ F₂) (U : Cᵒᵖ) : (Subpresheaf.equalizer f g).obj U = {x : F₁.obj U | ∃ (hx : x ∈ A.obj U), f.app U ⟨x, hx⟩ = g.app U ⟨x, hx⟩}

theorem CategoryTheory.Subpresheaf.equalizer_le {C : Type u} [Category.{v, u} C] {F₁ F₂ : Functor Cᵒᵖ (Type w)} {A : Subpresheaf F₁} (f g : A.toPresheaf ⟶ F₂) : Subpresheaf.equalizer f g ≤ A

@[simp]

theorem CategoryTheory.Subpresheaf.equalizer_self {C : Type u} [Category.{v, u} C] {F₁ F₂ : Functor Cᵒᵖ (Type w)} {A : Subpresheaf F₁} (f : A.toPresheaf ⟶ F₂) : Subpresheaf.equalizer f f = A

theorem CategoryTheory.Subpresheaf.mem_equalizer_iff {C : Type u} [Category.{v, u} C] {F₁ F₂ : Functor Cᵒᵖ (Type w)} {A : Subpresheaf F₁} (f g : A.toPresheaf ⟶ F₂) {i : Cᵒᵖ} (x : A.toPresheaf.obj i) : ↑x ∈ (Subpresheaf.equalizer f g).obj i ↔ f.app i x = g.app i x

theorem CategoryTheory.Subpresheaf.range_le_equalizer_iff {C : Type u} [Category.{v, u} C] {F₁ F₂ : Functor Cᵒᵖ (Type w)} {A : Subpresheaf F₁} (f g : A.toPresheaf ⟶ F₂) {G : Functor Cᵒᵖ (Type w)} (φ : G ⟶ A.toPresheaf) : range (CategoryStruct.comp φ A.ι) ≤ Subpresheaf.equalizer f g ↔ CategoryStruct.comp φ f = CategoryStruct.comp φ g

theorem CategoryTheory.Subpresheaf.equalizer_eq_iff {C : Type u} [Category.{v, u} C] {F₁ F₂ : Functor Cᵒᵖ (Type w)} {A : Subpresheaf F₁} (f g : A.toPresheaf ⟶ F₂) : Subpresheaf.equalizer f g = A ↔ f = g

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

Given two morphisms f and g in A.toPresheaf ⟶ F₂, this is the monomorphism of presheaves corresponding to the inclusion Subpresheaf.equalizer f g ≤ A.

instance CategoryTheory.Subpresheaf.instMonoFunctorOppositeTypeι_1 {C : Type u} [Category.{v, u} C] {F₁ F₂ : Functor Cᵒᵖ (Type w)} {A : Subpresheaf F₁} (f g : A.toPresheaf ⟶ F₂) : Mono (equalizer.ι f g)

@[simp]

theorem CategoryTheory.Subpresheaf.equalizer.ι_ι {C : Type u} [Category.{v, u} C] {F₁ F₂ : Functor Cᵒᵖ (Type w)} {A : Subpresheaf F₁} (f g : A.toPresheaf ⟶ F₂) : CategoryStruct.comp (ι f g) A.ι = (Subpresheaf.equalizer f g).ι

@[simp]

theorem CategoryTheory.Subpresheaf.equalizer.ι_ι_assoc {C : Type u} [Category.{v, u} C] {F₁ F₂ : Functor Cᵒᵖ (Type w)} {A : Subpresheaf F₁} (f g : A.toPresheaf ⟶ F₂) {Z : Functor Cᵒᵖ (Type w)} (h : F₁ ⟶ Z) : CategoryStruct.comp (ι f g) (CategoryStruct.comp A.ι h) = CategoryStruct.comp (Subpresheaf.equalizer f g).ι h

theorem CategoryTheory.Subpresheaf.equalizer.condition {C : Type u} [Category.{v, u} C] {F₁ F₂ : Functor Cᵒᵖ (Type w)} {A : Subpresheaf F₁} (f g : A.toPresheaf ⟶ F₂) : CategoryStruct.comp (ι f g) f = CategoryStruct.comp (ι f g) g

theorem CategoryTheory.Subpresheaf.equalizer.condition_assoc {C : Type u} [Category.{v, u} C] {F₁ F₂ : Functor Cᵒᵖ (Type w)} {A : Subpresheaf F₁} (f g : A.toPresheaf ⟶ 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)

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

The (limit) fork which expresses (Subpresheaf.equalizer f g).toPresheaf as the equalizer of f and g.

@[simp]

theorem CategoryTheory.Subpresheaf.equalizer.fork_pt {C : Type u} [Category.{v, u} C] {F₁ F₂ : Functor Cᵒᵖ (Type w)} {A : Subpresheaf F₁} (f g : A.toPresheaf ⟶ F₂) : (fork f g).pt = (Subpresheaf.equalizer f g).toPresheaf

@[simp]

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

def CategoryTheory.Subpresheaf.equalizer.forkIsLimit {C : Type u} [Category.{v, u} C] {F₁ F₂ : Functor Cᵒᵖ (Type w)} {A : Subpresheaf F₁} (f g : A.toPresheaf ⟶ F₂) : Limits.IsLimit (fork f g)

(Subpresheaf.equalizer f g).toPresheaf is the equalizer of f and g.