The depth function on periodic components

For the proof of Lemma 4.2 (lem:mesh-walk-free, scalar-normalization.tex): "A periodic component containing arrows gives a mapping torus, which retracts onto its core circle." By Proposition 4.1 a periodic component is covered by ℤΔ, and the deck transformations have the form (v, t) ↦ (ρ v, t + c₀) for a tree automorphism ρ (StarDeck.deck_height_form). "The automorphism ρ fixes a vertex or an edge midpoint of Δ" (lines 82–85): we use the centre of the path for type A, and the trivalent vertex for types D and E. The (doubled) distance to this centre is invariant under every deck transformation, so it descends to the component; each vertex has at most one neighbour at depth at most its own. This depth function drives the contraction onto the core circle in MeshComplex.lean.

def MultiplicativeBasisDeformations.StarDepth.cdep {t : ℕ} {L : Fin t → ℕ} (n : ℕ) (v : StarV L) : ℕ

The doubled distance from the centre at "half-depth" n / 2.

theorem MultiplicativeBasisDeformations.StarDepth.starAdj_symm {t : ℕ} {L : Fin t → ℕ} {a b : StarV L} (h : starAdj a b) : starAdj b a

theorem MultiplicativeBasisDeformations.StarDepth.depth_eq_zero {t : ℕ} {L : Fin t → ℕ} {v : StarV L} (h : starDepth v = 0) : v = none

theorem MultiplicativeBasisDeformations.StarDepth.depth_nb {t : ℕ} {L : Fin t → ℕ} (ht : 0 < t) {v : StarV L} (hv : v ≠ none) : starDepth (StarDeck.nb ht v) + 1 = starDepth v

theorem MultiplicativeBasisDeformations.StarDepth.depth_pres {t : ℕ} {L : Fin t → ℕ} (ht : 0 < t) (ρ : StarV L ≃ StarV L) (hρ : ∀ (a b : StarV L), starAdj a b ↔ starAdj (ρ a) (ρ b)) (h0 : ρ none = none) (n : ℕ) (v : StarV L) : starDepth v = n → starDepth (ρ v) = n

An automorphism fixing the centre preserves depth.

theorem MultiplicativeBasisDeformations.StarDepth.cdep_aut_path {L : Fin 1 → ℕ} (ρ : StarV L ≃ StarV L) (hρ : ∀ (a b : StarV L), starAdj a b ↔ starAdj (ρ a) (ρ b)) (v : StarV L) : cdep (L 0 + 1) (ρ v) = cdep (L 0 + 1) v

On a path, the distance to the middle is invariant under automorphisms.

theorem MultiplicativeBasisDeformations.StarDepth.cdep_aut_three {L : Fin 3 → ℕ} (ρ : StarV L ≃ StarV L) (hρ : ∀ (a b : StarV L), starAdj a b ↔ starAdj (ρ a) (ρ b)) (v : StarV L) : cdep 0 (ρ v) = cdep 0 v

With three arms, the depth is invariant under automorphisms.

theorem MultiplicativeBasisDeformations.StarDepth.cdep_uniq_path {L : Fin 1 → ℕ} (n : ℕ) {v w w' : StarV L} (hw : starAdj w v) (hw' : starAdj w' v) (h : cdep n w ≤ cdep n v) (h' : cdep n w' ≤ cdep n v) : w = w'

On a path, a vertex has at most one neighbour not farther from the middle.

theorem MultiplicativeBasisDeformations.StarDepth.cdep_uniq_zero {t : ℕ} {L : Fin t → ℕ} {v w w' : StarV L} (hw : starAdj w v) (hw' : starAdj w' v) (h : cdep 0 w ≤ cdep 0 v) (h' : cdep 0 w' ≤ cdep 0 v) : w = w'

A vertex has at most one neighbour not farther from the centre.

def MultiplicativeBasisDeformations.PeriodicDepth.IsDepth {W : Type u} [Quiver W] {Q : TranslationQuiver W} (hQ : Q.IsStable) (e : W → ℕ) : Prop

A depth function on a stable translation quiver: invariant under τ, and each vertex has at most one in-neighbour of depth at most its own.

theorem MultiplicativeBasisDeformations.PeriodicDepth.exists_depth_of_model {W : Type u} [Quiver W] [∀ (x y : W), Subsingleton (x ⟶ y)] {Q : TranslationQuiver W} (hQ : Q.IsStable) {t : ℕ} (L : Fin t → ℕ) (π : (starTree L).ZVert ⥤q W) (hπ : π.IsCovering) (hτ : ∀ (Y : (starTree L).ZVert), π.obj ((starTree L).ztau Y) = hQ.tauE (π.obj Y)) (hsurj : Function.Surjective π.obj) (ht : 0 < t) (f : StarV L → ℕ) (hf : ∀ (ρ : StarV L ≃ StarV L), (∀ (a b : StarV L), starAdj a b ↔ starAdj (ρ a) (ρ b)) → ∀ (v : StarV L), f (ρ v) = f v) (hu : ∀ {v w w' : StarV L}, starAdj w v → starAdj w' v → f w ≤ f v → f w' ≤ f v → w = w') : ∃ (e : W → ℕ), IsDepth hQ e

The depth function descends from the tree model.

theorem MultiplicativeBasisDeformations.PeriodicDepth.exists_depth {W : Type u} [Quiver W] [∀ (x y : W), Subsingleton (x ⟶ y)] {Q : TranslationQuiver W} (hQ : Q.IsStable) [Fintype W] [DecidableEq W] [(x y : W) → Fintype (x ⟶ y)] [(x : W) → Fintype ((y : W) × (y ⟶ x))] {k : Type u_1} [Field k] (c : MeshCoefficients k Q) (hfin : ∀ (x y : W), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)) (x₀ : W) (hconn : ∀ (v : W), Relation.EqvGen (TranslationQuiver.SecPath.ConnAdj hQ) x₀ v) : ∃ (e : W → ℕ), IsDepth hQ e

A connected periodic component has a depth function (Proposition 4.1 and the choice of a centre of Δ).

theorem MultiplicativeBasisDeformations.MeshWalk.cyclic_step {V : Type} [Quiver V] {Q : TranslationQuiver V} {y x : V} {a : y ⟶ x} (h : Cyclic Q ⟨y, ⟨x, a⟩⟩) : ∃ (hx : x ∈ Q.nonprojective), Cyclic Q ⟨↑(Q.tau ⟨x, hx⟩), ⟨y, (Q.mate ⟨x, hx⟩ y) a⟩⟩

theorem MultiplicativeBasisDeformations.MeshWalk.tauChain_of_cyclic {V : Type} [Quiver V] {Q : TranslationQuiver V} (n : ℕ) (A : Arr V) : Cyclic Q A → Q.TauChain A.snd.fst n ∧ Q.TauChain A.fst n

"A mate cycle forces periodic endpoints because σ² = τ."

theorem MultiplicativeBasisDeformations.MeshWalk.periodic_of_cyclic {V : Type} [Quiver V] {Q : TranslationQuiver V} {A : Arr V} (h : Cyclic Q A) : A.snd.fst ∈ Q.periodic ∧ A.fst ∈ Q.periodic

theorem MultiplicativeBasisDeformations.MeshWalk.component_eq {V : Type} [Quiver V] {Q : TranslationQuiver V} {u v : V} (h : Relation.EqvGen Q.PeriodicAdj u v) : Q.component u = Q.component v

theorem MultiplicativeBasisDeformations.MeshWalk.exists_depth_component {V : Type} [Quiver V] {Q : TranslationQuiver V} [Fintype V] [DecidableEq V] [∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [(x : V) → Fintype ((y : V) × (y ⟶ x))] {k : Type u_1} [Field k] (c : MeshCoefficients k Q) (hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)) (x : V) (hx : x ∈ Q.periodic) : ∃ (f : FullSub (Q.component x) → ℕ), PeriodicDepth.IsDepth ⋯ f

noncomputable def MultiplicativeBasisDeformations.MeshWalk.depthOn {V : Type} [Quiver V] {Q : TranslationQuiver V} [Fintype V] [DecidableEq V] [∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [(x : V) → Fintype ((y : V) × (y ⟶ x))] {k : Type u_1} [Field k] (c : MeshCoefficients k Q) (hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)) (S : Set V) (v : V) : ℕ

The depth on the vertices of a periodic component S, through the chosen model of S.

noncomputable def MultiplicativeBasisDeformations.MeshWalk.depth {V : Type} [Quiver V] {Q : TranslationQuiver V} [Fintype V] [DecidableEq V] [∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [(x : V) → Fintype ((y : V) × (y ⟶ x))] {k : Type u_1} [Field k] (c : MeshCoefficients k Q) (hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)) (v : V) : ℕ

The glued depth function.

theorem MultiplicativeBasisDeformations.MeshWalk.depth_spec {V : Type} [Quiver V] {Q : TranslationQuiver V} [Fintype V] [DecidableEq V] [∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [(x : V) → Fintype ((y : V) × (y ⟶ x))] {k : Type u_1} [Field k] (c : MeshCoefficients k Q) (hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)) (x : V) (hx : x ∈ Q.periodic) : ∃ (x₀ : V) (f : FullSub (Q.component x₀) → ℕ), PeriodicDepth.IsDepth ⋯ f ∧ Q.component x₀ = Q.component x ∧ ∀ (u : V) (hu : u ∈ Q.component x₀), Q.component u = Q.component x → depth c hfin u = f (FullSub.mk u hu)

theorem MultiplicativeBasisDeformations.MeshWalk.comp_arrow {V : Type} [Quiver V] {Q : TranslationQuiver V} [Fintype V] [DecidableEq V] [∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [(x : V) → Fintype ((y : V) × (y ⟶ x))] {y x : V} (hy : y ∈ Q.periodic) (hx : x ∈ Q.periodic) (a : y ⟶ x) : Q.component y = Q.component x

theorem MultiplicativeBasisDeformations.MeshWalk.comp_tau {V : Type} [Quiver V] {Q : TranslationQuiver V} [Fintype V] [DecidableEq V] [∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [(x : V) → Fintype ((y : V) × (y ⟶ x))] {x : V} (hx : x ∈ Q.periodic) (hn : x ∈ Q.nonprojective) : Q.component ↑(Q.tau ⟨x, hn⟩) = Q.component x

noncomputable def MultiplicativeBasisDeformations.MeshWalk.meshDepth {V : Type} [Quiver V] {Q : TranslationQuiver V} [Fintype V] [DecidableEq V] [∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [(x : V) → Fintype ((y : V) × (y ⟶ x))] {k : Type u_1} [Field k] (c : MeshCoefficients k Q) (hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)) : Depth Q

The depth function of Γ, from the tree models of its periodic components.

theorem MultiplicativeBasisDeformations.MeshWalk.isFreeGroup_end {V : Type} [Quiver V] {Q : TranslationQuiver V} [Fintype V] [DecidableEq V] [∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [(x : V) → Fintype ((y : V) × (y ⟶ x))] {k : Type u_1} [Field k] (c : MeshCoefficients k Q) (hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)) (X : V) : IsFreeGroup (CategoryTheory.End (obK Q X))

Lemma 4.2 (lem:mesh-walk-free) for a finite translation quiver with at most one arrow between two vertices and a finite-dimensional scalar mesh category: every vertex group of the complex K is free.