Lemma 12.3: gr_𝔪 B ≅ C

lem:flat-mesh-perturbations (deformation-refinements.tex): "Then gr_𝔪 B ≅ C." In each degree d, paths induce a linear isomorphism from C_d(w, y) (the image of the degree-d paths in C) onto 𝔪^d B(w, y)/𝔪^{d+1} B(w, y) (grIso); composition is induced by composition of paths on both sides. The map is well defined since a homogeneous relation u r v of degree d is u (r − f) v + u f v with u f v ∈ 𝔪^{d+1} (hctx_le_B_succ), onto since paths of length > d lie in 𝔪^{d+1} (sub_proj_mem_geSpan_succ), and bijective by counting: the degree projections make C graded (πC), so Σ_d dim C_d ≤ dim C, while Σ_d dim gr^d B = dim B = dim C (Lemma 12.3's dimension equality).

The degree projections of C

theorem MultiplicativeBasisDeformations.FlatPert.hctx_le_ctx {k : Type u} [Field k] {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (P : Pres k V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] [Fintype V] [(x y : V) → Fintype (x ⟶ y)] (d : ℕ) (w y : V) : hctx P d w y ≤ ctxSpan P P.r w y

theorem MultiplicativeBasisDeformations.FlatPert.proj_ctx_mem {k : Type u} [Field k] {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (P : Pres k V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] [Fintype V] [(x y : V) → Fintype (x ⟶ y)] (d : ℕ) {w y : V} {g : Hm k w y} (hg : g ∈ ctxSpan P P.r w y) : (LinearPaths.proj d w y) g ∈ ctxSpan P P.r w y

noncomputable def MultiplicativeBasisDeformations.FlatPert.πC {k : Type u} [Field k] {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (P : Pres k V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] [Fintype V] [(x y : V) → Fintype (x ⟶ y)] (d : ℕ) (w y : V) : Q (idealC P) w y →ₗ[k] Q (idealC P) w y

The degree-d projection of C.

theorem MultiplicativeBasisDeformations.FlatPert.πC_mk {k : Type u} [Field k] {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (P : Pres k V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] [Fintype V] [(x y : V) → Fintype (x ⟶ y)] (d : ℕ) {w y : V} (g : Hm k w y) : (πC P d w y) (Submodule.Quotient.mk g) = Submodule.Quotient.mk ((LinearPaths.proj d w y) g)

noncomputable def MultiplicativeBasisDeformations.FlatPert.CD {k : Type u} [Field k] {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (P : Pres k V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] (d : ℕ) (w y : V) : Submodule k (Q (idealC P) w y)

C_d(w, y): the image of the degree-d paths.

theorem MultiplicativeBasisDeformations.FlatPert.πC_mem {k : Type u} [Field k] {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (P : Pres k V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] [Fintype V] [(x y : V) → Fintype (x ⟶ y)] (d : ℕ) {w y : V} (x : Q (idealC P) w y) : (πC P d w y) x ∈ CD P d w y

theorem MultiplicativeBasisDeformations.FlatPert.πC_of_mem {k : Type u} [Field k] {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (P : Pres k V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] [Fintype V] [(x y : V) → Fintype (x ⟶ y)] {d e : ℕ} {w y : V} {x : Q (idealC P) w y} (hx : x ∈ CD P e w y) : (πC P d w y) x = if e = d then x else 0

The filtration of B

noncomputable def MultiplicativeBasisDeformations.FlatPert.FB {k : Type u} [Field k] {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (P : Pres k V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] (f : (x : V) → (t : P.T x) → Hm k (P.src x t) x) (hf : ∀ (x : V) (t : P.T x), f x t ∈ geSpan k (P.deg x t + 1) (P.src x t) x) (N d : ℕ) (w y : V) : Submodule k (Q (idealB P f hf N) w y)

𝔪^d B(w, y).

theorem MultiplicativeBasisDeformations.FlatPert.FB_anti {k : Type u} [Field k] {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (P : Pres k V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] (f : (x : V) → (t : P.T x) → Hm k (P.src x t) x) (hf : ∀ (x : V) (t : P.T x), f x t ∈ geSpan k (P.deg x t + 1) (P.src x t) x) (N : ℕ) [Fintype V] [(x y : V) → Fintype (x ⟶ y)] {d d' : ℕ} (h : d ≤ d') (w y : V) : FB P f hf N d' w y ≤ FB P f hf N d w y

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.FlatPert.grB {k : Type u} [Field k] {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (P : Pres k V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] (f : (x : V) → (t : P.T x) → Hm k (P.src x t) x) (hf : ∀ (x : V) (t : P.T x), f x t ∈ geSpan k (P.deg x t + 1) (P.src x t) x) (N d : ℕ) (w y : V) : Type u

gr^d B(w, y) = 𝔪^d B/𝔪^{d+1} B.

theorem MultiplicativeBasisDeformations.FlatPert.hctx_le_B_succ {k : Type u} [Field k] {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (P : Pres k V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] (f : (x : V) → (t : P.T x) → Hm k (P.src x t) x) (hf : ∀ (x : V) (t : P.T x), f x t ∈ geSpan k (P.deg x t + 1) (P.src x t) x) (N : ℕ) [Fintype V] [(x y : V) → Fintype (x ⟶ y)] (d : ℕ) (w y : V) : hctx P d w y ≤ (idealB P f hf N).I w y ⊔ geSpan k (d + 1) w y

theorem MultiplicativeBasisDeformations.FlatPert.sub_proj_mem_geSpan_succ {k : Type u} [Field k] {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [(x : V) → Fintype ((y : V) × (y ⟶ x))] [Fintype V] [(x y : V) → Fintype (x ⟶ y)] {d : ℕ} {w y : V} {g : Hm k w y} (hg : g ∈ geSpan k d w y) : g - (LinearPaths.proj d w y) g ∈ geSpan k (d + 1) w y

The map induced by paths

noncomputable def MultiplicativeBasisDeformations.FlatPert.ψC {k : Type u} [Field k] {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (P : Pres k V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] (d : ℕ) (w y : V) : ↥(LinearPaths.degreePart d w y) →ₗ[k] Q (idealC P) w y

Degree-d elements of kQ in C.

theorem MultiplicativeBasisDeformations.FlatPert.range_ψC {k : Type u} [Field k] {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (P : Pres k V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] [Fintype V] [(x y : V) → Fintype (x ⟶ y)] (d : ℕ) (w y : V) : (ψC P d w y).range = CD P d w y

noncomputable def MultiplicativeBasisDeformations.FlatPert.θ₀ {k : Type u} [Field k] {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (P : Pres k V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] (f : (x : V) → (t : P.T x) → Hm k (P.src x t) x) (hf : ∀ (x : V) (t : P.T x), f x t ∈ geSpan k (P.deg x t + 1) (P.src x t) x) (N d : ℕ) (w y : V) : ↥(LinearPaths.degreePart d w y) →ₗ[k] grB P f hf N d w y

Degree-d elements of kQ in gr^d B.

theorem MultiplicativeBasisDeformations.FlatPert.θ₀_apply {k : Type u} [Field k] {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (P : Pres k V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] (f : (x : V) → (t : P.T x) → Hm k (P.src x t) x) (hf : ∀ (x : V) (t : P.T x), f x t ∈ geSpan k (P.deg x t + 1) (P.src x t) x) (N : ℕ) [Fintype V] [(x y : V) → Fintype (x ⟶ y)] (d : ℕ) {w y : V} (g : ↥(LinearPaths.degreePart d w y)) : (θ₀ P f hf N d w y) g = Submodule.Quotient.mk ⟨Submodule.Quotient.mk ↑g, ⋯⟩

theorem MultiplicativeBasisDeformations.FlatPert.θ₀_surjective {k : Type u} [Field k] {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (P : Pres k V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] (f : (x : V) → (t : P.T x) → Hm k (P.src x t) x) (hf : ∀ (x : V) (t : P.T x), f x t ∈ geSpan k (P.deg x t + 1) (P.src x t) x) (N : ℕ) [Fintype V] [(x y : V) → Fintype (x ⟶ y)] (d : ℕ) (w y : V) : Function.Surjective ⇑(θ₀ P f hf N d w y)

theorem MultiplicativeBasisDeformations.FlatPert.ker_ψC_le {k : Type u} [Field k] {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (P : Pres k V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] (f : (x : V) → (t : P.T x) → Hm k (P.src x t) x) (hf : ∀ (x : V) (t : P.T x), f x t ∈ geSpan k (P.deg x t + 1) (P.src x t) x) (N : ℕ) [Fintype V] [(x y : V) → Fintype (x ⟶ y)] (d : ℕ) (w y : V) : (ψC P d w y).ker ≤ (θ₀ P f hf N d w y).ker

noncomputable def MultiplicativeBasisDeformations.FlatPert.θ {k : Type u} [Field k] {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (P : Pres k V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] (f : (x : V) → (t : P.T x) → Hm k (P.src x t) x) (hf : ∀ (x : V) (t : P.T x), f x t ∈ geSpan k (P.deg x t + 1) (P.src x t) x) (N : ℕ) [Fintype V] [(x y : V) → Fintype (x ⟶ y)] (d : ℕ) (w y : V) : ↥(CD P d w y) →ₗ[k] grB P f hf N d w y

The map C_d → gr^d B induced by paths.

theorem MultiplicativeBasisDeformations.FlatPert.θ_ψC {k : Type u} [Field k] {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (P : Pres k V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] (f : (x : V) → (t : P.T x) → Hm k (P.src x t) x) (hf : ∀ (x : V) (t : P.T x), f x t ∈ geSpan k (P.deg x t + 1) (P.src x t) x) (N : ℕ) [Fintype V] [(x y : V) → Fintype (x ⟶ y)] (d : ℕ) {w y : V} (g : ↥(LinearPaths.degreePart d w y)) : (θ P f hf N d w y) ⟨(ψC P d w y) g, ⋯⟩ = (θ₀ P f hf N d w y) g

theorem MultiplicativeBasisDeformations.FlatPert.θ_surjective {k : Type u} [Field k] {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (P : Pres k V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] (f : (x : V) → (t : P.T x) → Hm k (P.src x t) x) (hf : ∀ (x : V) (t : P.T x), f x t ∈ geSpan k (P.deg x t + 1) (P.src x t) x) (N : ℕ) [Fintype V] [(x y : V) → Fintype (x ⟶ y)] (d : ℕ) (w y : V) : Function.Surjective ⇑(θ P f hf N d w y)

Counting dimensions

theorem MultiplicativeBasisDeformations.FlatPert.FB_zero {k : Type u} [Field k] {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (P : Pres k V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] (f : (x : V) → (t : P.T x) → Hm k (P.src x t) x) (hf : ∀ (x : V) (t : P.T x), f x t ∈ geSpan k (P.deg x t + 1) (P.src x t) x) (N : ℕ) [Fintype V] [(x y : V) → Fintype (x ⟶ y)] (w y : V) : FB P f hf N 0 w y = ⊤

theorem MultiplicativeBasisDeformations.FlatPert.FB_eq_bot {k : Type u} [Field k] {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (P : Pres k V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] (f : (x : V) → (t : P.T x) → Hm k (P.src x t) x) (hf : ∀ (x : V) (t : P.T x), f x t ∈ geSpan k (P.deg x t + 1) (P.src x t) x) (N : ℕ) [Fintype V] [(x y : V) → Fintype (x ⟶ y)] {d : ℕ} (hd : N + 1 ≤ d) (w y : V) : FB P f hf N d w y = ⊥

theorem MultiplicativeBasisDeformations.FlatPert.finrank_grB_add {k : Type u} [Field k] {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (P : Pres k V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] (f : (x : V) → (t : P.T x) → Hm k (P.src x t) x) (hf : ∀ (x : V) (t : P.T x), f x t ∈ geSpan k (P.deg x t + 1) (P.src x t) x) (N : ℕ) [Fintype V] [(x y : V) → Fintype (x ⟶ y)] (d : ℕ) (w y : V) [Module.Finite k (Q (idealB P f hf N) w y)] : Module.finrank k (grB P f hf N d w y) + Module.finrank k ↥(FB P f hf N (d + 1) w y) = Module.finrank k ↥(FB P f hf N d w y)

theorem MultiplicativeBasisDeformations.FlatPert.sum_grB {k : Type u} [Field k] {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (P : Pres k V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] (f : (x : V) → (t : P.T x) → Hm k (P.src x t) x) (hf : ∀ (x : V) (t : P.T x), f x t ∈ geSpan k (P.deg x t + 1) (P.src x t) x) (N : ℕ) [Fintype V] [(x y : V) → Fintype (x ⟶ y)] (w y : V) [Module.Finite k (Q (idealB P f hf N) w y)] (M : ℕ) : ∑ d ∈ Finset.range M, Module.finrank k (grB P f hf N d w y) + Module.finrank k ↥(FB P f hf N M w y) = Module.finrank k ↥(FB P f hf N 0 w y)

theorem MultiplicativeBasisDeformations.FlatPert.sum_CD_le {k : Type u} [Field k] {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (P : Pres k V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] [Fintype V] [(x y : V) → Fintype (x ⟶ y)] (w y : V) [Module.Finite k (Q (idealC P) w y)] (M : ℕ) : ∑ d ∈ Finset.range M, Module.finrank k ↥(CD P d w y) ≤ Module.finrank k (Q (idealC P) w y)

theorem MultiplicativeBasisDeformations.FlatPert.grIso_of_finrank {k : Type u} [Field k] {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (P : Pres k V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] (f : (x : V) → (t : P.T x) → Hm k (P.src x t) x) (hf : ∀ (x : V) (t : P.T x), f x t ∈ geSpan k (P.deg x t + 1) (P.src x t) x) (N : ℕ) [Fintype V] [(x y : V) → Fintype (x ⟶ y)] (hN : ∀ (w y : V) (p : Quiver.Path w y), N ≤ p.length → LinearPaths.path p ∈ ctxSpan P P.r w y) (hdim : ∀ (w y : V), Module.finrank k (Q (idealB P f hf N) w y) = Module.finrank k (Q (idealC P) w y)) (d : ℕ) (w y : V) : ∃ (e : ↥(CD P d w y) ≃ₗ[k] grB P f hf N d w y), ∀ (g : ↥(LinearPaths.degreePart d w y)), e ⟨(ψC P d w y) g, ⋯⟩ = (θ₀ P f hf N d w y) g

gr_𝔪 B ≅ C from the equality of the dimensions of B and C.

theorem MultiplicativeBasisDeformations.FlatPert.grIso {k : Type u} [Field k] {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (P : Pres k V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] (f : (x : V) → (t : P.T x) → Hm k (P.src x t) x) (hf : ∀ (x : V) (t : P.T x), f x t ∈ geSpan k (P.deg x t + 1) (P.src x t) x) (N : ℕ) [Fintype V] [(x y : V) → Fintype (x ⟶ y)] (hN : ∀ (w y : V) (p : Quiver.Path w y), N ≤ p.length → LinearPaths.path p ∈ ctxSpan P P.r w y) (hC : ∀ (w x : V), Function.Injective ⇑(relMap P (idealC P) P.r w x) ∧ (alpha (idealC P) w x).ker ≤ (relMap P (idealC P) P.r w x).range) (d : ℕ) (w y : V) : ∃ (e : ↥(CD P d w y) ≃ₗ[k] grB P f hf N d w y), ∀ (g : ↥(LinearPaths.degreePart d w y)), e ⟨(ψC P d w y) g, ⋯⟩ = (θ₀ P f hf N d w y) g

Lemma 12.3, gr_𝔪 B ≅ C: in every degree d, paths induce a linear isomorphism C_d(w, y) ≅ 𝔪^d B(w, y)/𝔪^{d+1} B(w, y).