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
🔸 coverage
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
    Instances For
      source
      📐 coverage
      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
      📐 coverage
      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
      📐 coverage
      @[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
      📐 coverage
      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
      📐 coverage
      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
      📐 coverage
      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
      🔸 coverage
      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
          📐 coverage
          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
          📐 coverage
          @[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
          📐 coverage
          @[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
          📐 coverage
          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
          📐 coverage
          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
          🔸 coverage
          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
              📐 coverage
              @[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
              📐 coverage
              @[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
              📐 coverage
              @[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
              📐 coverage
              @[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
              🔸 coverage
              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
                  📐 coverage
                  @[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
                  📐 coverage
                  @[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
                  🔸 coverage
                  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
                    Instances For
                      source
                      🔸 coverage
                      @[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
                        Instances For
                          source
                          📐 coverage
                          @[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
                          📐 coverage
                          @[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
                          📐 coverage
                          @[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
                          📐 coverage
                          @[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
                          📐 coverage
                          @[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
                          🔸 coverage
                          @[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
                            Instances For
                              source
                              📐 coverage
                              @[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
                              📐 coverage
                              @[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
                              🔸 coverage
                              @[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.

                              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
                                  📐 coverage
                                  @[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
                                  📐 coverage
                                  @[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
                                  🔸 coverage
                                  @[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
                                    Instances For
                                      source
                                      📐 coverage
                                      @[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
                                      🔸 coverage
                                      @[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
                                        Instances For