LeanPool.Polylean.Complexes.Structures.Category

Imported Lean Pool material for LeanPool.Polylean.Complexes.Structures.Category.

class LeanPool.Polylean.CategoryStruct (Obj : Sort u_1) extends LeanPool.Polylean.Quiver Obj : Sort (max u_1 (u_2 + 1))

The definition of a CategoryStruct, a barebones structure for a category containing none of the axioms (following mathlib).

• hom : Obj → Obj → Sort u_2
• id (X : Obj) : X ⟶ X

  The identity morphism at an object.

• comp {X Y Z : Obj} : (X ⟶ Y) → (Y ⟶ Z) → (X ⟶ Z)

  Composition of composable morphisms.

def LeanPool.Polylean.«term𝟙» : Lean.ParserDescr

Identity morphism notation.

Equations

• LeanPool.Polylean.«term𝟙» = Lean.ParserDescr.node `LeanPool.Polylean.«term𝟙» 1024 (Lean.ParserDescr.symbol "𝟙")

def LeanPool.Polylean.«term_≫_» : Lean.TrailingParserDescr

Morphism composition notation.

Equations

• LeanPool.Polylean.«term_≫_» = Lean.ParserDescr.trailingNode `LeanPool.Polylean.«term_≫_» 80 81 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≫ ") (Lean.ParserDescr.cat `term 80))

def LeanPool.Polylean.«term_⊚_» : Lean.TrailingParserDescr

Reverse-order morphism composition notation.

Equations

• LeanPool.Polylean.«term_⊚_» = Lean.ParserDescr.trailingNode `LeanPool.Polylean.«term_⊚_» 80 80 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊚ ") (Lean.ParserDescr.cat `term 81))

class LeanPool.Polylean.Category (Obj : Sort u_1) extends LeanPool.Polylean.CategoryStruct Obj : Sort (max u_1 (u_2 + 1))

The definition of a Category.

• hom : Obj → Obj → Sort u_2
• id (X : Obj) : X ⟶ X
• comp {X Y Z : Obj} : (X ⟶ Y) → (Y ⟶ Z) → (X ⟶ Z)
• id_comp {X Y : Obj} (f : X ⟶ Y) : 𝟙 X ≫ f = f
• comp_id {X Y : Obj} (f : X ⟶ Y) : f ≫ 𝟙 Y = f
• comp_assoc {W X Y Z : Obj} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z) : (f ≫ g) ≫ h = f ≫ g ≫ h

structure LeanPool.Polylean.Category.Functor {C : Sort u_1} {D : Sort u_2} (𝓒 : Category C) (𝓓 : Category D) extends 𝓒.PreFunctor 𝓓.toQuiver : Sort (max (max (max (max 1 u_1) u_2) u_3) u_4)

A functor is a morphism of categories.

• obj : C → D
• map {X Y : C} : (X ⟶ Y) → (self.obj X ⟶ self.obj Y)
• map_id (X : C) : self.map (𝟙 X) = 𝟙 (self.obj X)
• map_comp {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : self.map (f ≫ g) = self.map f ≫ self.map g

def LeanPool.Polylean.Category.Functor.«term_⥤_» : Lean.TrailingParserDescr

Functor notation between categories.

Equations

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

def LeanPool.Polylean.Category.Functor.id (C : Sort u_1) [𝓒 : Category C] : 𝓒 ⥤ 𝓒

The identity functor.

Equations

• LeanPool.Polylean.Category.Functor.id C = { obj := id, map := fun {X Y : C} => id, map_id := ⋯, map_comp := ⋯ }

def LeanPool.Polylean.Category.Functor.comp {C : Sort u_1} {D : Sort u_2} {E : Sort u_3} {𝓒 : Category C} {𝓓 : Category D} {𝓔 : Category E} (F : 𝓒 ⥤ 𝓓) (G : 𝓓 ⥤ 𝓔) : 𝓒 ⥤ 𝓔

Composition of functors.

Equations

• F ⋙ G = { obj := G.obj ∘ F.obj, map := fun {X Y : C} => G.map ∘ F.map, map_id := ⋯, map_comp := ⋯ }

def LeanPool.Polylean.Category.Functor.«term_⋙_» : Lean.TrailingParserDescr

Functor composition notation.

Equations

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

@[simp]

theorem LeanPool.Polylean.Category.Functor.comp_obj {Obj✝ : Sort u_1} {Obj✝¹ : Sort u_2} {𝓒✝ : Category Obj✝} {𝓓✝ : Category Obj✝¹} {Ψ : 𝓒✝ ⥤ 𝓓✝} {Obj✝² : Sort u_5} {𝓓✝¹ : Category Obj✝²} {Φ : 𝓓✝ ⥤ 𝓓✝¹} : Φ.obj ∘ Ψ.obj = (Ψ ⋙ Φ).obj

The object map of a composed functor is the composite object map.

@[simp]

theorem LeanPool.Polylean.Category.Functor.comp_obj' {Obj✝ : Sort u_1} {Obj✝¹ : Sort u_2} {𝓒✝ : Category Obj✝} {𝓓✝ : Category Obj✝¹} {Ψ : 𝓒✝ ⥤ 𝓓✝} {Obj✝² : Sort u_5} {𝓓✝¹ : Category Obj✝²} {Φ : 𝓓✝ ⥤ 𝓓✝¹} (x : Obj✝) : Φ.obj (Ψ.obj x) = (Ψ ⋙ Φ).obj x

Pointwise form of Category.Functor.comp_obj.

def LeanPool.Polylean.Path.compose {C : Sort u_1} [𝓒 : Category C] {X Y : C} : Path X Y → (X ⟶ Y)

Compose the arrows appearing in a category path.

Equations

• LeanPool.Polylean.Path.nil.compose = 𝟙 X
• (LeanPool.Polylean.Path.cons e p).compose = e ≫ p.compose

@[simp]

theorem LeanPool.Polylean.Path.compose_nil {C : Sort u_2} [𝓒 : Category C] {X : C} : (nil' X).compose = 𝟙 X

theorem LeanPool.Polylean.Path.compose_append {C : Sort u_1} [𝓒 : Category C] {X Y Z : C} {p : Path X Y} {q : Path Y Z} : (p.append q).compose = p.compose ≫ q.compose

Composing an appended path equals composing the two pieces.

@[implicit_reducible, instance 100]

instance LeanPool.Polylean.Quiver.PathCategory {V : Sort u_1} [Quiver V] : Category V

Paths in a quiver form a category under concatenation.

Equations

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

def LeanPool.Polylean.Quiver.toPathCategory {V : Sort u_1} [Q : Quiver V] : Q.PreFunctor PathCategory.toQuiver

Embedding of a Quiver into its category of paths.

Equations

• LeanPool.Polylean.Quiver.toPathCategory = { obj := id, map := fun {X Y : V} => LeanPool.Polylean.Quiver.toPath }