Documentation

Mathlib.CategoryTheory.Subfunctor.Equalizer

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
  • One or more equations did not get rendered due to their size.
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), (ConcreteCategory.hom (f.app U)) ⟨x, hx⟩ = (ConcreteCategory.hom (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 ↔ (ConcreteCategory.hom (f.app i)) x = (ConcreteCategory.hom (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
    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
      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
        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