Documentation

CKMath.Category.Functor

structure Category.Functor {OA : Sort u_1} {OB : Sort u_2} (A : OAOASort v_A) (B : OBOBSort v_B) [𝓐 : Category A] [𝓑 : Category B] :
Sort (max (max (max (max 1 u_1) u_2) v_A) v_B)

The basic data of a Functor, consisting of a map between the arrows of a category.

  • obj : OAOB

    A map from objects of A to objects of B.

  • map : {x y : OA} → A x yB (self.obj x) (self.obj y)

    A map from maps in A to maps on the corresponding objects in B.

  • map_id : ∀ {x : OA}, self.map Category.Struct.id = Category.Struct.id

    The functor respects identity.

  • map_comp : ∀ {x x_1 : OA} {f : A x x_1} {x_2 : OA} {g : A x_1 x_2}, self.map (f g) = self.map f self.map g

    The functor respects composition.

Instances For
    theorem Category.Functor.ext {OA : Sort u_1} {OB : Sort u_2} {A : OAOASort v_A} {B : OBOBSort v_B} {𝓐 : Category A} {𝓑 : Category B} {x y : A B} (obj : x.obj = y.obj) (map : HEq (@Category.Functor.map OA OB A B 𝓐 𝓑 x) (@Category.Functor.map OA OB A B 𝓐 𝓑 y)) :
    x = y
    def Category.Functor.id {OA : Sort u_1} {A : OAOASort v_A} [𝓐 : Category A] :
    A A
    Equations
    • Category.Functor.id = { obj := fun (x : OA) => x, map := fun {x y : OA} (f : A x y) => f, map_id := , map_comp := }
    Instances For
      def Category.Functor.comp {OA : Sort u_1} {OB : Sort u_2} {OD : Sort u_3} {A : OAOASort v_A} {B : OBOBSort v_B} {C : ODODSort v_D} [𝓐 : Category A] [𝓑 : Category B] [𝓒 : Category C] (F : A B) (G : B C) :
      A C
      Equations
      • F G = { obj := G.obj F.obj, map := fun {x y : OA} => G.map F.map, map_id := , map_comp := }
      Instances For
        @[simp]
        def Category.Functor.pre_id {OA : Sort u_1} {OB : Sort u_2} {A : OAOASort v_A} {B : OBOBSort v_B} [𝓐 : Category A] [𝓑 : Category B] {F : A B} :
        Category.Functor.id F = F
        Equations
        • =
        Instances For
          @[simp]
          def Category.Functor.post_id {OA : Sort u_1} {OB : Sort u_2} {A : OAOASort v_A} {B : OBOBSort v_B} [𝓐 : Category A] [𝓑 : Category B] {F : A B} :
          F Category.Functor.id = F
          Equations
          • =
          Instances For
            @[simp]
            def Category.Functor.comp_assoc {OA : Sort u_1} {OB : Sort u_2} {OD : Sort u_3} {x✝ : Sort u_5} {D : x✝x✝Sort u_4} {A : OAOASort v_A} {B : OBOBSort v_B} {C : ODODSort v_D} [𝓐 : Category A] [𝓑 : Category B] [𝓒 : Category C] [𝓓 : Category D] {F : A B} {G : B C} {H : C D} :
            (F G) H = F G H
            Equations
            • =
            Instances For
              structure Category.Nat {OA : Sort u_1} {OB : Sort u_2} (A : OAOASort v_A) (B : OBOBSort v_B) [𝓐 : Category A] [𝓑 : Category B] (F G : A B) :
              Sort (max (max 1 u_1) v_B)
              • on : (x : OA) → B (F.obj x) (G.obj x)
              • natural : ∀ {x y : OA} {f : A x y}, self.on x G.map f = F.map f self.on y
              Instances For
                theorem Category.Nat.ext {OA : Sort u_1} {OB : Sort u_2} {A : OAOASort v_A} {B : OBOBSort v_B} {𝓐 : Category A} {𝓑 : Category B} {F G : A B} {x y : Category.Nat A B F G} (on : x.on = y.on) :
                x = y
                @[simp]
                theorem Category.Nat.eq_iff_on_eq {OA : Sort u_1} {OB : Sort u_2} {A : OAOASort v_A} {B : OBOBSort v_B} [𝓐 : Category A] [𝓑 : Category B] {F G : A B} {α β : Category.Nat A B F G} :
                α = β ∀ (x : OA), α.on x = β.on x
                def Category.Nat.id {OA : Sort u_1} {OB : Sort u_2} {A : OAOASort v_A} {B : OBOBSort v_B} [𝓐 : Category A] [𝓑 : Category B] {F : A B} :
                Category.Nat A B F F
                Equations
                • Category.Nat.id = { on := fun (x : OA) => Category.Struct.id, natural := }
                Instances For
                  def Category.Nat.comp {OA : Sort u_1} {OB : Sort u_2} {A : OAOASort v_A} {B : OBOBSort v_B} [𝓐 : Category A] [𝓑 : Category B] {F G H : A B} (α : Category.Nat A B F G) (β : Category.Nat A B G H) :
                  Category.Nat A B F H
                  Equations
                  • α.comp β = { on := fun (x : OA) => α.on x β.on x, natural := }
                  Instances For
                    instance Category.Nat.categoryStruct {OA : Sort u_1} {OB : Sort u_2} {A : OAOASort v_A} {B : OBOBSort v_B} [𝓐 : Category A] [𝓑 : Category B] :
                    Equations
                    • Category.Nat.categoryStruct = { id := fun {x : A B} => Category.Nat.id, comp := fun {a b c : A B} => Category.Nat.comp }
                    @[simp]
                    theorem Category.Nat.id_on {OA : Sort u_1} {OB : Sort u_2} {A : OAOASort v_A} {B : OBOBSort v_B} [𝓐 : Category A] [𝓑 : Category B] {x : OA} {F : A B} :
                    Category.Nat.id.on x = Category.Struct.id
                    @[simp]
                    theorem Category.Nat.comp_on {OA : Sort u_1} {OB : Sort u_2} {A : OAOASort v_A} {B : OBOBSort v_B} [𝓐 : Category A] [𝓑 : Category B] {F G H : A B} {α : Category.Nat A B F G} {β : Category.Nat A B G H} {x : OA} :
                    (α β).on x = α.on x β.on x
                    instance Category.Nat.category {OA : Sort u_1} {OB : Sort u_2} {A : OAOASort v_A} {B : OBOBSort v_B} [𝓐 : Category A] [𝓑 : Category B] :
                    Equations
                    def Category.whisker_pre {OA : Sort u_1} {OB : Sort u_2} {OC : Sort u_3} {A : OAOASort v_A} {B : OBOBSort v_B} {C : OCOCSort v_C} [𝓐 : Category A] [𝓑 : Category B] [𝓒 : Category C] (H : B C) :
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      @[simp]
                      def Category.whisker_pre_on {OA : Sort u_3} {OB : Sort u_1} {OC : Sort u_2} {A : OAOASort v_A} {B : OBOBSort v_B} {C : OCOCSort v_C} [𝓐 : Category A] [𝓑 : Category B] [𝓒 : Category C] {H : B C} {F0 F1 : A B} {α : Category.Nat A B F0 F1} {x : OA} :
                      ((Category.whisker_pre H).map α).on x = H.map (α.on x)
                      Equations
                      • =
                      Instances For
                        def Category.whisker_post {OA : Sort u_1} {OB : Sort u_2} {OC : Sort u_3} {A : OAOASort v_A} {B : OBOBSort v_B} {C : OCOCSort v_C} [𝓐 : Category A] [𝓑 : Category B] [𝓒 : Category C] (H : A B) :
                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          @[simp]
                          def Category.whisker_post_on {OA : Sort u_1} {OB : Sort u_2} {OC : Sort u_3} {A : OAOASort v_A} {B : OBOBSort v_B} {C : OCOCSort v_C} [𝓐 : Category A] [𝓑 : Category B] [𝓒 : Category C] {H : A B} {F0 F1 : B C} {α : Category.Nat B C F0 F1} {x : OA} :
                          ((Category.whisker_post H).map α).on x = α.on (H.obj x)
                          Equations
                          • =
                          Instances For
                            @[reducible, inline]
                            abbrev Category.Nat.hcomp_post_pre {OA : Sort u_1} {OB : Sort u_2} {OC : Sort u_3} {A : OAOASort v_A} {B : OBOBSort v_B} {C : OCOCSort v_C} [𝓐 : Category A] [𝓑 : Category B] [𝓒 : Category C] {F0 F1 : A B} {G0 G1 : B C} (α : Category.Nat A B F0 F1) (β : Category.Nat B C G0 G1) :
                            Category.Nat A C (F0 G0) (F1 G1)
                            Equations
                            Instances For
                              @[reducible, inline]
                              abbrev Category.Nat.hcomp_pre_post {OA : Sort u_1} {OB : Sort u_2} {OC : Sort u_3} {A : OAOASort v_A} {B : OBOBSort v_B} {C : OCOCSort v_C} [𝓐 : Category A] [𝓑 : Category B] [𝓒 : Category C] {F0 F1 : A B} {G0 G1 : B C} (α : Category.Nat A B F0 F1) (β : Category.Nat B C G0 G1) :
                              Category.Nat A C (F0 G0) (F1 G1)
                              Equations
                              Instances For
                                theorem Category.Nat.hcomp_pre_post_eq_post_pre {OA : Sort u_1} {OB : Sort u_3} {OC : Sort u_2} {A : OAOASort v_A} {B : OBOBSort v_B} {C : OCOCSort v_C} [𝓐 : Category A] [𝓑 : Category B] [𝓒 : Category C] {F0 F1 : A B} {G0 G1 : B C} (α : Category.Nat A B F0 F1) (β : Category.Nat B C G0 G1) :
                                α.hcomp_pre_post β = α.hcomp_post_pre β
                                def Category.Nat.hcomp {OA : Sort u_1} {OB : Sort u_2} {OC : Sort u_3} {A : OAOASort v_A} {B : OBOBSort v_B} {C : OCOCSort v_C} [𝓐 : Category A] [𝓑 : Category B] [𝓒 : Category C] {F0 F1 : A B} {G0 G1 : B C} (α : Category.Nat A B F0 F1) (β : Category.Nat B C G0 G1) :
                                Category.Nat A C (F0 G0) (F1 G1)
                                Equations
                                • α.hcomp β = α.hcomp_post_pre β
                                Instances For
                                  theorem Category.Nat.hcomp_vcomp_is_vcomp_hcomp {OA : Sort u_1} {OB : Sort u_3} {OC : Sort u_2} {A : OAOASort v_A} {B : OBOBSort v_B} {C : OCOCSort v_C} [𝓐 : Category A] [𝓑 : Category B] [𝓒 : Category C] {F0 F1 F2 : A B} {G0 G1 G2 : B C} (α0 : Category.Nat A B F0 F1) (α1 : Category.Nat A B F1 F2) (β0 : Category.Nat B C G0 G1) (β1 : Category.Nat B C G1 G2) :
                                  (α0 α1).hcomp (β0 β1) = α0.hcomp β0 α1.hcomp β1

                                  Horizontal composition is compatible with vertical composition in a natural way.

                                  def Category.Nat.hcomp_id_id {OA : Sort u_1} {OB : Sort u_3} {OC : Sort u_2} {A : OAOASort v_A} {B : OBOBSort v_B} {C : OCOCSort v_C} [𝓐 : Category A] [𝓑 : Category B] [𝓒 : Category C] {F0 : A B} {G0 : B C} :
                                  Category.Nat.id.hcomp Category.Nat.id = Category.Nat.id
                                  Equations
                                  • =
                                  Instances For