LeanPool.Polylean.Complexes.GraphPaths

structure LeanPool.Polylean.Graph (V E : Type) : Type

A graph with directed edges, distinguished null edge, and edge reversal.

• null : E

  The distinguished null edge.

• init : E → V

  The initial vertex of an edge.

• bar : E → E

  The reverse of an edge.

• barInv : self.bar ∘ self.bar = id
• barNoFP (e : E) : self.bar e ≠ e

@[inline]

def LeanPool.Polylean.term {V E : Type} (graph : Graph V E) : E → V

The terminal vertex of an edge, defined as the initial vertex of its reverse.

Equations

• LeanPool.Polylean.term graph e = graph.init (graph.bar e)

inductive LeanPool.Polylean.EdgePath {V E : Type} (graph : Graph V E) : V → V → Type

Edge paths in a graph, indexed by their initial and terminal vertices.

• single {V E : Type} {graph : Graph V E} (x : V) : EdgePath graph x x
• cons {V E : Type} {graph : Graph V E} {x y z : V} (e : E) : graph.init e = x → term graph e = y → EdgePath graph y z → EdgePath graph x z

def LeanPool.Polylean.EdgePath.length {V E : Type} {graph : Graph V E} {x y : V} : EdgePath graph x y → ℕ

The number of edges in an edge path.

Equations

• (LeanPool.Polylean.EdgePath.single y).length = 0
• (LeanPool.Polylean.EdgePath.cons e a a_1 path).length = path.length + 1

theorem LeanPool.Polylean.bar_involution {V E : Type} {G : Graph V E} (ex : E) : G.bar (G.bar ex) = ex

proves that bar is an involution

def LeanPool.Polylean.multiply {V E : Type} {G : Graph V E} {x y z : V} : EdgePath G x y → EdgePath G y z → EdgePath G x z

concatenates two edgepaths

Equations

• LeanPool.Polylean.multiply (LeanPool.Polylean.EdgePath.single y) q = q
• LeanPool.Polylean.multiply (LeanPool.Polylean.EdgePath.cons ex h1 h2 exy) q = LeanPool.Polylean.EdgePath.cons ex h1 h2 (LeanPool.Polylean.multiply exy q)

theorem LeanPool.Polylean.term_bar_equals_init {V E : Type} {G : Graph V E} {x : V} {e : E} : G.init e = x → term G (G.bar e) = x

proves that the endpoint of the reverse of an edge is the start point of the edge

theorem LeanPool.Polylean.init_bar_equals_term {V E : Type} {G : Graph V E} {x : V} {e : E} : term G e = x → G.init (G.bar e) = x

proves that initial vertex of reversed edge is the terminal vertex of the original edge

theorem LeanPool.Polylean.mult_assoc {V E : Type} {w x y z : V} {G : Graph V E} (p : EdgePath G w x) (q : EdgePath G x y) (r : EdgePath G y z) : multiply (multiply p q) r = multiply p (multiply q r)

proves associativity of path multiplication

theorem LeanPool.Polylean.mult_const {V E : Type} {x y : V} {G : Graph V E} (p : EdgePath G x y) : multiply p (EdgePath.single y) = p

proves that "single x" is an identity element for multiplication

def LeanPool.Polylean.inverse {V E : Type} {G : Graph V E} {x y : V} : EdgePath G x y → EdgePath G y x

reverses an edgepath

Equations

• One or more equations did not get rendered due to their size.
• LeanPool.Polylean.inverse (LeanPool.Polylean.EdgePath.single y) = LeanPool.Polylean.EdgePath.single y

def LeanPool.Polylean.basicpath {V E : Type} {y : V} {G : Graph V E} (x : V) (ex : E) (h₁ : G.init ex = x) (h₂ : term G ex = y) : EdgePath G x y

defines an edgepath with a single edge

Equations

• LeanPool.Polylean.basicpath x ex h₁ h₂ = LeanPool.Polylean.EdgePath.cons ex h₁ h₂ (LeanPool.Polylean.EdgePath.single y)

theorem LeanPool.Polylean.basicpath_mult {V E : Type} {G : Graph V E} {x y z : V} (ex : E) (h₁ : G.init ex = x) (h₂ : term G ex = y) (exy : EdgePath G y z) : multiply (basicpath x ex h₁ h₂) exy = EdgePath.cons ex h₁ h₂ exy

proves that multiplication with a basicpath gives inductive definition of edgepath

theorem LeanPool.Polylean.inverse_lemma {V E : Type} {G : Graph V E} {x y z : V} (ex : E) (h₁ : G.init ex = x) (h₂ : term G ex = y) (exy : EdgePath G y z) : inverse (EdgePath.cons ex h₁ h₂ exy) = multiply (inverse exy) (basicpath y (G.bar ex) h₂ ⋯)

defines inverse in terms of basicpath

theorem LeanPool.Polylean.inverse_mult {V E : Type} {G : Graph V E} (x y z : V) (p : EdgePath G x y) (q : EdgePath G y z) : inverse (multiply p q) = multiply (inverse q) (inverse p)

proves the basic relation between inverse and multiply

theorem LeanPool.Polylean.inverse_involution {V E : Type} {G : Graph V E} {x y : V} (p : EdgePath G x y) : inverse (inverse p) = p

proves that inverse is an involution on paths

def LeanPool.Polylean.reducePathAux {V E : Type} [DecidableEq V] [DecidableEq E] {G : Graph V E} {x y z : V} (ex : E) (h₁ : G.init ex = x) (h₂ : term G ex = y) (exy : EdgePath G y z) : { rp : EdgePath G x z // rp.length ≤ (EdgePath.cons ex h₁ h₂ exy).length }

helper function for reducePath, that reduces the first two edges of the path

Equations

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

@[irreducible]

def LeanPool.Polylean.reducePath {V E : Type} {x y : V} [DecidableEq V] [DecidableEq E] {G : Graph V E} (p : EdgePath G x y) : { rp : EdgePath G x y // rp.length ≤ p.length }

reduces given path such that no two consecutive edges are inverses of each other

Equations

• One or more equations did not get rendered due to their size.
• LeanPool.Polylean.reducePath (LeanPool.Polylean.EdgePath.single y) = ⟨LeanPool.Polylean.EdgePath.single y, ⋯⟩

inductive LeanPool.Polylean.basicht {V E : Type} {G : Graph V E} {x y : V} : EdgePath G x y → EdgePath G x y → Prop

defines moves allowing homotopy of edgepaths

• consht {V E : Type} {G : Graph V E} (x : V) : basicht (EdgePath.single x) (EdgePath.single x)
• cancel {V E : Type} {G : Graph V E} (ex ex' : E) {x w y : V} (p : EdgePath G x y) (h : G.init ex = x) (h' : term G ex = w) (t : G.bar ex = ex') : basicht p (EdgePath.cons ex h h' (EdgePath.cons ex' ⋯ ⋯ p))
• mult {V E : Type} {G : Graph V E} {x y z : V} {p q : EdgePath G y z} : basicht p q → ∀ (ex : E) (h' : G.init ex = x) (h : term G ex = y), basicht (EdgePath.cons ex h' h p) (EdgePath.cons ex h' h q)

def LeanPool.Polylean.ht {V E : Type} (G : Graph V E) (x y : V) : Type

The set of homotopy classes of edge paths from x to y.

Equations

• LeanPool.Polylean.ht G x y = Quot LeanPool.Polylean.basicht

def LeanPool.Polylean.htclass {V E : Type} {G : Graph V E} {x y : V} (p : EdgePath G x y) : ht G x y

The homotopy class of an edge path.

Equations

• LeanPool.Polylean.htclass p = Quot.mk LeanPool.Polylean.basicht p

def LeanPool.Polylean.homotopy {V E : Type} {G : Graph V E} {x y : V} (p' q' : EdgePath G x y) : Prop

Homotopy of edge paths as equality of their quotient classes.

Equations

• LeanPool.Polylean.homotopy p' q' = (LeanPool.Polylean.htclass p' = LeanPool.Polylean.htclass q')

theorem LeanPool.Polylean.homotopy_trans {V E : Type} {G : Graph V E} {x y : V} (p q r : EdgePath G x y) : homotopy p q → homotopy q r → homotopy p r

proves that homotopy is a transitive relation

theorem LeanPool.Polylean.homotopy_left_mult_edge {V E : Type} {G : Graph V E} {x y z : V} (p q : EdgePath G y z) : homotopy p q → ∀ (ex : E) (h1 : G.init ex = x) (h : term G ex = y), homotopy (EdgePath.cons ex h1 h p) (EdgePath.cons ex h1 h q)

proves that homotopy is preserved by multiplying an edge to the left

theorem LeanPool.Polylean.homotopy_left_mult {V E : Type} {G : Graph V E} {x y z : V} (p1 p2 : EdgePath G y z) (q : EdgePath G x y) (h : homotopy p1 p2) : homotopy (multiply q p1) (multiply q p2)

proves that homotopy is left multiplicative

theorem LeanPool.Polylean.homotopy_rfl {V E : Type} {G : Graph V E} {x y : V} (p : EdgePath G x y) : homotopy p p

proves that homotopy is reflexive

theorem LeanPool.Polylean.induct_homotopy_inverse_cancel {V E : Type} {G : Graph V E} (ey ey' : E) {x w y : V} (p : EdgePath G x y) (h₁ : G.init ey = y) (h₂ : term G ey = w) (t : G.bar ey = ey') (h₃ : G.init ey' = w) (h₄ : term G ey' = y) : homotopy p (multiply p (EdgePath.cons ey h₁ h₂ (EdgePath.cons ey' h₃ h₄ (EdgePath.single y))))

proves that path is homotopic to itself after appending cancelling pair of edges at its end

theorem LeanPool.Polylean.induct_homotopy_inverse_mult {V E : Type} {G : Graph V E} {x y z : V} (p q : EdgePath G x y) (ey : E) (h₁ : G.init ey = y) (h₂ : term G ey = z) : homotopy p q → homotopy (multiply p (basicpath y ey h₁ h₂)) (multiply q (basicpath y ey h₁ h₂))

proves that a pair of paths remains homotopic after appending a single edge at their ends

theorem LeanPool.Polylean.homotopy_inverse {V E : Type} {G : Graph V E} {x y : V} (p₁ p₂ : EdgePath G x y) (q₁ q₂ : EdgePath G y x) (h₁ : q₁ = inverse p₁) (h₂ : q₂ = inverse p₂) : homotopy p₁ p₂ → homotopy q₁ q₂

proves that homotopy of paths implies homotopy of their inverses

theorem LeanPool.Polylean.homotopy_inverse_quick {V E : Type} {G : Graph V E} {x y : V} {p₁ p₂ : EdgePath G x y} : homotopy p₁ p₂ → homotopy (inverse p₁) (inverse p₂)

homotopy_inverse with lesser arguments

theorem LeanPool.Polylean.homotopy_right_mult {V E : Type} {G : Graph V E} {x y z : V} (p₁ p₂ : EdgePath G x y) (q : EdgePath G y z) (h : homotopy p₁ p₂) : homotopy (multiply p₁ q) (multiply p₂ q)

proves that homotopy is right multiplicative

def LeanPool.Polylean.homotopyLeftMultiplication {V E : Type} {G : Graph V E} {x y z : V} (p₁ : EdgePath G x y) : ht G y z → ht G x z

defines multiplication of homotopy class with a path to its left

Equations

• LeanPool.Polylean.homotopyLeftMultiplication p₁ = Quot.lift (fun (p : LeanPool.Polylean.EdgePath G y z) => LeanPool.Polylean.htclass (LeanPool.Polylean.multiply p₁ p)) ⋯

theorem LeanPool.Polylean.homotopy_left_multiplication_class {V E : Type} {G : Graph V E} {x y z : V} (p₁ : EdgePath G x y) (p₂ : EdgePath G y z) : homotopyLeftMultiplication p₁ (htclass p₂) = htclass (multiply p₁ p₂)

proves that the multiplication defined above equals homotopy class of multiplied paths

def LeanPool.Polylean.homotopyMultiplication {V✝ E✝ : Type} {G : Graph V✝ E✝} {x y z : V✝} : ht G x y → ht G y z → ht G x z

defines multiplication of homotopy

Equations

• p₁ # p₂ = Quot.lift (fun (x_1 : LeanPool.Polylean.EdgePath G x y) => (fun (p : LeanPool.Polylean.EdgePath G x y) => LeanPool.Polylean.homotopyLeftMultiplication p p₂) x_1) ⋯ p₁

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

Multiplication of homotopy classes of composable edge paths.

Equations

• LeanPool.Polylean.«term_#_» = Lean.ParserDescr.trailingNode `LeanPool.Polylean.«term_#_» 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " # ") (Lean.ParserDescr.cat `term 66))

theorem LeanPool.Polylean.homotopy_mult_path_path_assoc {V E : Type} {G : Graph V E} {w x y z : V} (p : EdgePath G w x) (q : EdgePath G x y) (r : ht G y z) : htclass (multiply p q) # r = htclass p # (htclass q # r)

proves that # is associative up to multiplication by a pair of paths and one homotopy class

theorem LeanPool.Polylean.homotopy_mult_path_assoc {V E : Type} {G : Graph V E} {w x y z : V} (p : EdgePath G w x) (r : ht G y z) (q : ht G x y) : htclass p # q # r = htclass p # (q # r)

proves that # is associative up to multiplication by one path and a pair of homotopy classes

theorem LeanPool.Polylean.homotopy_mult_assoc {V E : Type} {G : Graph V E} {w x y z : V} (b : ht G x y) (c : ht G y z) (a : ht G w x) : a # b # c = a # (b # c)

proves that # is associative on homotopy classes

theorem LeanPool.Polylean.homotopy_reducePathAux {V E : Type} [DecidableEq V] [DecidableEq E] {G : Graph V E} {x y z : V} (ex : E) (h₁ : G.init ex = x) (h₂ : term G ex = y) (exy : EdgePath G y z) : homotopy (EdgePath.cons ex h₁ h₂ exy) (reducePathAux ex h₁ h₂ exy).val

proves that reducePathAux preserves the homotopy class

theorem LeanPool.Polylean.homotopy_reducePath {V E : Type} [DecidableEq V] [DecidableEq E] {G : Graph V E} {x y : V} (p₁ : EdgePath G x y) : homotopy p₁ (reducePath p₁).val

proves that reducePath preserves the homotopy class

@[implicit_reducible]

instance LeanPool.Polylean.htMul {V E : Type} {G : Graph V E} {x : V} : Mul (ht G x x)

Equations

• LeanPool.Polylean.htMul = { mul := fun (a b : LeanPool.Polylean.ht G x x) => a # b }

@[implicit_reducible]

instance LeanPool.Polylean.htOne {V E : Type} {G : Graph V E} {x : V} : One (ht G x x)

Equations

• LeanPool.Polylean.htOne = { one := LeanPool.Polylean.htclass (LeanPool.Polylean.EdgePath.single x) }

theorem LeanPool.Polylean.ht_mult_assoc {V E : Type} {G : Graph V E} {x : V} (a b c : ht G x x) : a # b # c = a # (b # c)

proves that multiplication of homotopy classes is associative

theorem LeanPool.Polylean.ht_right_identity {V E : Type} {G : Graph V E} {x : V} (a₀ : ht G x x) : Mul.mul a₀ One.one = a₀

proves that the identity homotopy class is the right multiplicative identity

theorem LeanPool.Polylean.ht_left_identity {V E : Type} {G : Graph V E} {x : V} (a₀ : ht G x x) : Mul.mul One.one a₀ = a₀

proves that the identity homotopy class is the left multiplicative identity

@[implicit_reducible]

instance LeanPool.Polylean.htSemigroup {V E : Type} {G : Graph V E} {x : V} : Semigroup (ht G x x)

Equations

• LeanPool.Polylean.htSemigroup = { toMul := LeanPool.Polylean.htMul, mul_assoc := ⋯ }

@[reducible]

def LeanPool.Polylean.htMonoid {V E : Type} (G : Graph V E) (x : V) : Monoid (ht G x x)

The monoid structure on loops at a vertex modulo homotopy.

Equations

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