Collapsing a 2-complex along an acyclic matching

Combinatorial tool for Lemma 4.2 (lem:mesh-walk-free, scalar-normalization.tex). A 2-complex is given by edges Ed with endpoints and triangles t with relation f_t g_t = h_t; its fundamental groupoid Π is the free groupoid on the edges modulo these relations. Given an injective choice of one edge per triangle (a matching) with a potential strictly decreasing from a triangle to the triangles matching its other edges, each matched edge is expressed through the remaining ones — the source's "eliminate these edges and triangles from one end of the chain" — and Π is isomorphic to the free groupoid on the unmatched edges.

def MultiplicativeBasisDeformations.Morse.EQ {V Ed : Type} (_src _tgt : Ed → V) : Type

The quiver on V whose arrows are the edges.

@[instance_reducible]

instance MultiplicativeBasisDeformations.Morse.instQuiverEQ {V Ed : Type} (src tgt : Ed → V) : Quiver (EQ src tgt)

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.Morse.FG {V Ed : Type} (src tgt : Ed → V) : Type

The free groupoid on the edges.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.Morse.ob {V Ed : Type} (src tgt : Ed → V) (X : V) : FG src tgt

A vertex as an object of the free groupoid.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.Morse.ofE {V Ed : Type} (src tgt : Ed → V) (e : Ed) : ob src tgt (src e) ⟶ ob src tgt (tgt e)

An edge as a morphism of the free groupoid.

structure MultiplicativeBasisDeformations.Morse.Tris {V Ed : Type} (src tgt : Ed → V) : Type 1

Triangles f g = h.

• T : Type
• f : self.T → Ed
• g : self.T → Ed
• h : self.T → Ed
• hfg (t : self.T) : tgt (self.f t) = src (self.g t)
• hfh (t : self.T) : src (self.f t) = src (self.h t)
• hgh (t : self.T) : tgt (self.g t) = tgt (self.h t)

inductive MultiplicativeBasisDeformations.Morse.TriRel {V Ed : Type} {src tgt : Ed → V} (S : Tris src tgt) : HomRel (FG src tgt)

The triangle relations.

• tri {V Ed : Type} {src tgt : Ed → V} {S : Tris src tgt} (t : S.T) : TriRel S (CategoryTheory.CategoryStruct.comp (ofE src tgt (S.f t)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (ofE src tgt (S.g t)))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (ofE src tgt (S.h t)) (CategoryTheory.eqToHom ⋯)))

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.Morse.Pi {V Ed : Type} {src tgt : Ed → V} (S : Tris src tgt) : Type

The fundamental groupoid of the 2-complex.

def MultiplicativeBasisDeformations.Morse.Tris.edge {V Ed : Type} {src tgt : Ed → V} (S : Tris src tgt) (t : S.T) : Fin 3 → Ed

The three edges of a triangle.

structure MultiplicativeBasisDeformations.Morse.Matching {V Ed : Type} {src tgt : Ed → V} (S : Tris src tgt) : Type

An acyclic matching: one edge per triangle, injectively, with a potential decreasing from a triangle to the triangles matching its other edges.

• m : S.T → Fin 3
• inj : Function.Injective fun (t : S.T) => S.edge t (self.m t)
• pot : S.T → ℕ
• dec (t : S.T) (i : Fin 3) : i ≠ self.m t → ∀ (t' : S.T), S.edge t' (self.m t') = S.edge t i → self.pot t' < self.pot t

def MultiplicativeBasisDeformations.Morse.Matched {V Ed : Type} {src tgt : Ed → V} {S : Tris src tgt} (M : Matching S) (e : Ed) : Prop

An edge is matched if it is the chosen edge of a triangle.

def MultiplicativeBasisDeformations.Morse.UQ {V Ed : Type} {src tgt : Ed → V} {S : Tris src tgt} (_M : Matching S) : Type

The quiver of unmatched edges.

@[instance_reducible]

instance MultiplicativeBasisDeformations.Morse.instQuiverUQ {V Ed : Type} {src tgt : Ed → V} {S : Tris src tgt} (M : Matching S) : Quiver (UQ M)

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.Morse.FGU {V Ed : Type} {src tgt : Ed → V} {S : Tris src tgt} (M : Matching S) : Type

The free groupoid on the unmatched edges.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.Morse.obU {V Ed : Type} {src tgt : Ed → V} {S : Tris src tgt} (M : Matching S) (X : V) : FGU M

A vertex as an object of FGU.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.Morse.ofU {V Ed : Type} {src tgt : Ed → V} {S : Tris src tgt} (M : Matching S) (e : Ed) (he : ¬Matched M e) : obU M (src e) ⟶ obU M (tgt e)

An unmatched edge as a morphism of FGU.

noncomputable def MultiplicativeBasisDeformations.Morse.μ {V Ed : Type} {src tgt : Ed → V} {S : Tris src tgt} (M : Matching S) (e : Ed) : ℕ

The recursion measure.

theorem MultiplicativeBasisDeformations.Morse.μ_lt_of_other {V Ed : Type} {src tgt : Ed → V} {S : Tris src tgt} (M : Matching S) {e : Ed} (h : Matched M e) (i : Fin 3) (hi : i ≠ M.m (Classical.choose h)) : μ M (S.edge (Classical.choose h) i) < μ M e

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.Morse.Val {V Ed : Type} {src tgt : Ed → V} {S : Tris src tgt} (M : Matching S) (e : Ed) : Type

The type of values of an edge in FGU.

noncomputable def MultiplicativeBasisDeformations.Morse.edgeVal {V Ed : Type} {src tgt : Ed → V} {S : Tris src tgt} (M : Matching S) (e : Ed) (bound : ℕ) (rec : (t' : S.T) → M.pot t' < bound → Val M (S.edge t' (M.m t'))) (hb : ∀ (t' : S.T), S.edge t' (M.m t') = e → M.pot t' < bound) : Val M e

The value of an edge, given values on the triangles of smaller potential.

def MultiplicativeBasisDeformations.Morse.triVal {V Ed : Type} {src tgt : Ed → V} {S : Tris src tgt} (M : Matching S) (t : S.T) (i : Fin 3) : i = M.m t → ((j : Fin 3) → j ≠ M.m t → Val M (S.edge t j)) → Val M (S.edge t i)

The value of the matched edge i of t through the other two edges.

noncomputable def MultiplicativeBasisDeformations.Morse.ψ {V Ed : Type} {src tgt : Ed → V} {S : Tris src tgt} (M : Matching S) (t : S.T) : Val M (S.edge t (M.m t))

The values of the matched edges, by recursion on the potential.

theorem MultiplicativeBasisDeformations.Morse.ψ_eq {V Ed : Type} {src tgt : Ed → V} {S : Tris src tgt} (M : Matching S) (t : S.T) : ψ M t = triVal M t (M.m t) ⋯ fun (i : Fin 3) (hi : i ≠ M.m t) => edgeVal M (S.edge t i) (M.pot t) (fun (t' : S.T) (x : M.pot t' < M.pot t) => ψ M t') ⋯

noncomputable def MultiplicativeBasisDeformations.Morse.φ {V Ed : Type} {src tgt : Ed → V} {S : Tris src tgt} (M : Matching S) (e : Ed) : Val M e

The value of an arbitrary edge.

theorem MultiplicativeBasisDeformations.Morse.edgeVal_eq {V Ed : Type} {src tgt : Ed → V} {S : Tris src tgt} (M : Matching S) (e : Ed) (bound : ℕ) (hb : ∀ (t' : S.T), S.edge t' (M.m t') = e → M.pot t' < bound) : edgeVal M e bound (fun (t' : S.T) (x : M.pot t' < bound) => ψ M t') hb = φ M e

edgeVal agrees with φ.

theorem MultiplicativeBasisDeformations.Morse.φ_matched {V Ed : Type} {src tgt : Ed → V} {S : Tris src tgt} (M : Matching S) (t : S.T) : φ M (S.edge t (M.m t)) = ψ M t

φ at the matched edge of t is ψ t.

theorem MultiplicativeBasisDeformations.Morse.φ_unmatched {V Ed : Type} {src tgt : Ed → V} {S : Tris src tgt} (M : Matching S) (e : Ed) (h : ¬Matched M e) : φ M e = ofU M e h

theorem MultiplicativeBasisDeformations.Morse.φ_tri {V Ed : Type} {src tgt : Ed → V} {S : Tris src tgt} (M : Matching S) (t : S.T) (i : Fin 3) (hi : i = M.m t) : φ M (S.edge t i) = triVal M t i hi fun (j : Fin 3) (x : j ≠ M.m t) => φ M (S.edge t j)

theorem MultiplicativeBasisDeformations.Morse.φ_f {V Ed : Type} {src tgt : Ed → V} {S : Tris src tgt} (M : Matching S) (t : S.T) (h0 : M.m t = 0) : φ M (S.f t) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (φ M (S.h t)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Groupoid.inv (φ M (S.g t))) (CategoryTheory.eqToHom ⋯))))

theorem MultiplicativeBasisDeformations.Morse.φ_g {V Ed : Type} {src tgt : Ed → V} {S : Tris src tgt} (M : Matching S) (t : S.T) (h1 : M.m t = 1) : φ M (S.g t) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Groupoid.inv (φ M (S.f t))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (φ M (S.h t)) (CategoryTheory.eqToHom ⋯))))

theorem MultiplicativeBasisDeformations.Morse.φ_h {V Ed : Type} {src tgt : Ed → V} {S : Tris src tgt} (M : Matching S) (t : S.T) (h2 : M.m t = 2) : φ M (S.h t) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (φ M (S.f t)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (φ M (S.g t)) (CategoryTheory.eqToHom ⋯))))

theorem MultiplicativeBasisDeformations.Morse.φ_rel {V Ed : Type} {src tgt : Ed → V} {S : Tris src tgt} (M : Matching S) (t : S.T) : CategoryTheory.CategoryStruct.comp (φ M (S.f t)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (φ M (S.g t))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (φ M (S.h t)) (CategoryTheory.eqToHom ⋯))

The triangle relations hold in FGU.

noncomputable def MultiplicativeBasisDeformations.Morse.Φ0 {V Ed : Type} {src tgt : Ed → V} {S : Tris src tgt} (M : Matching S) : EQ src tgt ⥤q FGU M

The prefunctor sending an edge to its value.

noncomputable def MultiplicativeBasisDeformations.Morse.Φ1 {V Ed : Type} {src tgt : Ed → V} {S : Tris src tgt} (M : Matching S) : CategoryTheory.Functor (FG src tgt) (FGU M)

Its extension to the free groupoid.

theorem MultiplicativeBasisDeformations.Morse.Φ1_obj {V Ed : Type} {src tgt : Ed → V} {S : Tris src tgt} (M : Matching S) (X : V) : (Φ1 M).obj (ob src tgt X) = obU M X

theorem MultiplicativeBasisDeformations.Morse.Φ1_ofE {V Ed : Type} {src tgt : Ed → V} {S : Tris src tgt} (M : Matching S) (e : Ed) : (Φ1 M).map (ofE src tgt e) = φ M e

theorem MultiplicativeBasisDeformations.Morse.Φ1_rel {V Ed : Type} {src tgt : Ed → V} {S : Tris src tgt} (M : Matching S) (X Y : FG src tgt) (f₁ f₂ : X ⟶ Y) : TriRel S f₁ f₂ → (Φ1 M).map f₁ = (Φ1 M).map f₂

noncomputable def MultiplicativeBasisDeformations.Morse.Φ {V Ed : Type} {src tgt : Ed → V} {S : Tris src tgt} (M : Matching S) : CategoryTheory.Functor (Pi S) (FGU M)

The collapse functor Π → FGU.

def MultiplicativeBasisDeformations.Morse.Ψ0 {V Ed : Type} {src tgt : Ed → V} {S : Tris src tgt} (M : Matching S) : UQ M ⥤q Pi S

The inclusion of the unmatched edges, as a prefunctor into Π.

def MultiplicativeBasisDeformations.Morse.Ψ {V Ed : Type} {src tgt : Ed → V} {S : Tris src tgt} (M : Matching S) : CategoryTheory.Functor (FGU M) (Pi S)

The inclusion functor FGU → Π.

theorem MultiplicativeBasisDeformations.Morse.Ψ_ofU {V Ed : Type} {src tgt : Ed → V} {S : Tris src tgt} (M : Matching S) (e : Ed) (he : ¬Matched M e) : (Ψ M).map (ofU M e he) = (CategoryTheory.Quotient.functor (TriRel S)).map (ofE src tgt e)

theorem MultiplicativeBasisDeformations.Morse.eqToHom_sandwich {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X X' Y Y' : C} (p : X = X') (q : X' = X) (f : X ⟶ Y) (r : Y = Y') (s : Y' = Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom p) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom q) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom r) (CategoryTheory.eqToHom s)))) = f

theorem MultiplicativeBasisDeformations.Morse.eqToHom_conj_self {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} (p : X = X) (q : Y = Y) (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom p) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom q)) = f

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.Morse.Qf {V Ed : Type} {src tgt : Ed → V} {S : Tris src tgt} : CategoryTheory.Functor (FG src tgt) (CategoryTheory.Quotient (TriRel S))

The quotient functor onto Π.

theorem MultiplicativeBasisDeformations.Morse.Q_rel {V Ed : Type} {src tgt : Ed → V} {S : Tris src tgt} (t : S.T) : CategoryTheory.CategoryStruct.comp (Qf.map (ofE src tgt (S.f t))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (Qf.map (ofE src tgt (S.g t)))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (Qf.map (ofE src tgt (S.h t))) (CategoryTheory.eqToHom ⋯))

theorem MultiplicativeBasisDeformations.Morse.Ψ_φ {V Ed : Type} {src tgt : Ed → V} {S : Tris src tgt} (M : Matching S) (e : Ed) : (Ψ M).map (φ M e) = Qf.map (ofE src tgt e)

theorem MultiplicativeBasisDeformations.Morse.Φ_Qf_map {V Ed : Type} {src tgt : Ed → V} {S : Tris src tgt} (M : Matching S) {X Y : FG src tgt} (f : X ⟶ Y) : (Φ M).map (Qf.map f) = (Φ1 M).map f

theorem MultiplicativeBasisDeformations.Morse.ΨΦ {V Ed : Type} {src tgt : Ed → V} {S : Tris src tgt} (M : Matching S) : (Ψ M).comp (Φ M) = CategoryTheory.Functor.id (FGU M)

theorem MultiplicativeBasisDeformations.Morse.ΦΨ {V Ed : Type} {src tgt : Ed → V} {S : Tris src tgt} (M : Matching S) : (Φ M).comp (Ψ M) = CategoryTheory.Functor.id (Pi S)

noncomputable def MultiplicativeBasisDeformations.Morse.endMulEquiv {V Ed : Type} {src tgt : Ed → V} {S : Tris src tgt} (M : Matching S) (X : V) : CategoryTheory.End (Qf.obj (ob src tgt X)) ≃* CategoryTheory.End (obU M X)

Collapse on vertex groups: π₁(K, X) is the vertex group of the free groupoid on the unmatched edges.

theorem MultiplicativeBasisDeformations.Morse.isFreeGroup_end {V Ed : Type} {src tgt : Ed → V} {S : Tris src tgt} (M : Matching S) (X : V) : IsFreeGroup (CategoryTheory.End (Qf.obj (ob src tgt X)))

The vertex groups of a collapsible 2-complex are free.