Documentation

Mathlib.CategoryTheory.Subpresheaf.Equalizer

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.

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

Equations
Instances For
    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}

    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.

    Equations
    Instances For

      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.

      Equations
      Instances For
        @[simp]

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

        Equations
        Instances For
          @[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

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

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For