Documentation

LeanPool.Polylean.Complexes.Structures.Groupoid

LeanPool.Polylean.Complexes.Structures.Groupoid #

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

class LeanPool.Polylean.Groupoid (S : Sort u_1) extends LeanPool.Polylean.Category S :

Sort (max u_1 (u_2 + 1))

A Groupoid is defined as a Category in which every morphism has an inverse satisfying certain conditions.

hom : S → S → Sort u_2
id (X : S) : X ⟶ X
comp {X Y Z : S} : (X ⟶ Y) → (Y ⟶ Z) → (X ⟶ Z)
id_comp {X Y : S} (f : X ⟶ Y) : 𝟙 X ≫ f = f
comp_id {X Y : S} (f : X ⟶ Y) : f ≫ 𝟙 Y = f
comp_assoc {W X Y Z : S} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z) : (f ≫ g) ≫ h = f ≫ g ≫ h
inv {X Y : S} : (X ⟶ Y) → (Y ⟶ X)
The inverse of a morphism.
inv_comp_id {X Y : S} (g : X ⟶ Y) : g ⁻¹ ≫ g = 𝟙 Y
comp_inv_id {X Y : S} (g : X ⟶ Y) : g ≫ g ⁻¹ = 𝟙 X

Instances

def LeanPool.Polylean.Groupoid.«term_⁻¹» :

Lean.TrailingParserDescr

Groupoid inverse notation.

Equations

LeanPool.Polylean.Groupoid.«term_⁻¹» = Lean.ParserDescr.trailingNode `LeanPool.Polylean.Groupoid.«term_⁻¹» 1024 1024 (Lean.ParserDescr.symbol " ⁻¹ ")

Instances For

@[simp]

theorem LeanPool.Polylean.Groupoid.left_inv_cancel {S : Sort u_2} [G : Groupoid S] {X Y Z : S} (g : X ⟶ Y) (h : Y ⟶ Z) :

g ⁻¹ ≫ g ≫ h = h

@[simp]

theorem LeanPool.Polylean.Groupoid.id_inv {S : Sort u_2} [G : Groupoid S] {X : S} :

(𝟙 X) ⁻¹ = 𝟙 X

@[simp]

theorem LeanPool.Polylean.Groupoid.inv_inv {S : Sort u_2} [G : Groupoid S] {X Y : S} (g : X ⟶ Y) :

g ⁻¹ ⁻¹ = g

@[simp]

theorem LeanPool.Polylean.Groupoid.left_cancel_inv {S : Sort u_1} [G : Groupoid S] {X Y Z : S} (g : X ⟶ Y) (h : X ⟶ Z) :

g ≫ g ⁻¹ ≫ h = h

@[simp]

theorem LeanPool.Polylean.Groupoid.inv_comp {S : Sort u_2} [G : Groupoid S] {X Y Z : S} (g : X ⟶ Y) (h : Y ⟶ Z) :

(g ≫ h) ⁻¹ = h ⁻¹ ≫ g ⁻¹

@[simp]

theorem LeanPool.Polylean.Groupoid.left_cancel {S : Sort u_2} [G : Groupoid S] {X Y Z : S} (g : X ⟶ Y) (h h' : Y ⟶ Z) :

g ≫ h = g ≫ h' ↔ h = h'

@[simp]

theorem LeanPool.Polylean.Groupoid.right_cancel {S : Sort u_2} [G : Groupoid S] {X Y Z : S} (g g' : X ⟶ Y) (h : Y ⟶ Z) :

g ≫ h = g' ≫ h ↔ g = g'

@[simp]

theorem LeanPool.Polylean.Groupoid.left_cancel_id {S : Sort u_1} [G : Groupoid S] {X Y : S} (g : X ⟶ Y) {e : Y ⟶ Y} :

g = g ≫ e ↔ 𝟙 Y = e

@[simp]

theorem LeanPool.Polylean.Groupoid.left_cancel_id' {S : Sort u_1} [G : Groupoid S] {X Y : S} (g : X ⟶ Y) {e : Y ⟶ Y} :

g ≫ e = g ↔ e = 𝟙 Y

@[simp]

theorem LeanPool.Polylean.Groupoid.right_cancel_id {S : Sort u_1} [G : Groupoid S] {X Y : S} (g : X ⟶ Y) {e : X ⟶ X} :

g = e ≫ g ↔ 𝟙 X = e

@[simp]

theorem LeanPool.Polylean.Groupoid.right_cancel_id' {S : Sort u_1} [G : Groupoid S] {X Y : S} (g : X ⟶ Y) {e : X ⟶ X} :

e ≫ g = g ↔ e = 𝟙 X

structure LeanPool.Polylean.Groupoid.Functor {S : Sort u_1} {S' : Sort u_2} (G : Groupoid S) (G' : Groupoid S') extends G.toCategory ⥤ G'.toCategory :

Sort (max (max (max (max 1 u_1) u_2) u_3) u_4)

A Functor is a morphism of Groupoids.

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

Instances For

theorem LeanPool.Polylean.Groupoid.Functor.map_id' {S : Sort u_3} {T : Sort u_2} [G : Groupoid S] [H : Groupoid T] (Φ : G.Functor H) {X : S} :

Φ.map (𝟙 X) = 𝟙 (Φ.obj X)

@[simp]

theorem LeanPool.Polylean.Groupoid.Functor.map_inv {S : Sort u_1} {T : Sort u_4} [G : Groupoid S] [H : Groupoid T] (Φ : G.Functor H) {X Y : S} (g : X ⟶ Y) :

Φ.map g ⁻¹ = (Φ.map g) ⁻¹