structure
Category.Functor
{OA : Sort u_1}
{OB : Sort u_2}
(A : OA → OA → Sort v_A)
(B : OB → OB → Sort 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 : OA → OB
A map from objects of A to objects of B.
- map : {x y : OA} → A x y → B (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 : OA → OA → Sort v_A}
{B : OB → OB → Sort 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
Equations
- Category.«term_⥤_» = Lean.ParserDescr.trailingNode `Category.«term_⥤_» 90 91 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⥤ ") (Lean.ParserDescr.cat `term 90))
Instances For
Equations
- Category.Functor.«term_⋙_» = Lean.ParserDescr.trailingNode `Category.Functor.«term_⋙_» 85 86 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⋙ ") (Lean.ParserDescr.cat `term 85))
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 : OA → OA → Sort v_A}
{B : OB → OB → Sort v_B}
{C : OD → OD → Sort v_D}
[𝓐 : Category A]
[𝓑 : Category B]
[𝓒 : Category C]
[𝓓 : Category D]
{F : A ⥤ B}
{G : B ⥤ C}
{H : C ⥤ D}
:
Equations
- ⋯ = ⋯
Instances For
Equations
- Category.«term_⇓_» = Lean.ParserDescr.trailingNode `Category.«term_⇓_» 81 82 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⇓ ") (Lean.ParserDescr.cat `term 81))
Instances For
def
Category.Nat.comp
{OA : Sort u_1}
{OB : Sort u_2}
{A : OA → OA → Sort v_A}
{B : OB → OB → Sort 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
Instances For
instance
Category.Nat.categoryStruct
{OA : Sort u_1}
{OB : Sort u_2}
{A : OA → OA → Sort v_A}
{B : OB → OB → Sort v_B}
[𝓐 : Category A]
[𝓑 : Category B]
:
Category.Struct (Category.Nat A B)
@[simp]
theorem
Category.Nat.comp_on
{OA : Sort u_1}
{OB : Sort u_2}
{A : OA → OA → Sort v_A}
{B : OB → OB → Sort 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}
:
instance
Category.Nat.category
{OA : Sort u_1}
{OB : Sort u_2}
{A : OA → OA → Sort v_A}
{B : OB → OB → Sort v_B}
[𝓐 : Category A]
[𝓑 : Category B]
:
Category (Category.Nat A B)
Equations
- Category.Nat.category = Category.mk ⋯ ⋯ ⋯
def
Category.whisker_pre
{OA : Sort u_1}
{OB : Sort u_2}
{OC : Sort u_3}
{A : OA → OA → Sort v_A}
{B : OB → OB → Sort v_B}
{C : OC → OC → Sort v_C}
[𝓐 : Category A]
[𝓑 : Category B]
[𝓒 : Category C]
(H : B ⥤ C)
:
Category.Nat A B ⥤ Category.Nat A 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 : OA → OA → Sort v_A}
{B : OB → OB → Sort v_B}
{C : OC → OC → Sort 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 : OA → OA → Sort v_A}
{B : OB → OB → Sort v_B}
{C : OC → OC → Sort v_C}
[𝓐 : Category A]
[𝓑 : Category B]
[𝓒 : Category C]
(H : A ⥤ B)
:
Category.Nat B C ⥤ Category.Nat A C
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 : OA → OA → Sort v_A}
{B : OB → OB → Sort v_B}
{C : OC → OC → Sort 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 : OA → OA → Sort v_A}
{B : OB → OB → Sort v_B}
{C : OC → OC → Sort 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_post_pre β = (Category.whisker_post F0).map β ≫ (Category.whisker_pre G1).map α
Instances For
@[reducible, inline]
abbrev
Category.Nat.hcomp_pre_post
{OA : Sort u_1}
{OB : Sort u_2}
{OC : Sort u_3}
{A : OA → OA → Sort v_A}
{B : OB → OB → Sort v_B}
{C : OC → OC → Sort 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_pre_post β = (Category.whisker_pre G0).map α ≫ (Category.whisker_post F1).map β
Instances For
theorem
Category.Nat.hcomp_pre_post_eq_post_pre
{OA : Sort u_1}
{OB : Sort u_3}
{OC : Sort u_2}
{A : OA → OA → Sort v_A}
{B : OB → OB → Sort v_B}
{C : OC → OC → Sort 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 : OA → OA → Sort v_A}
{B : OB → OB → Sort v_B}
{C : OC → OC → Sort 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 : OA → OA → Sort v_A}
{B : OB → OB → Sort v_B}
{C : OC → OC → Sort 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)
:
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 : OA → OA → Sort v_A}
{B : OB → OB → Sort v_B}
{C : OC → OC → Sort 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
- ⋯ = ⋯