Lemma 12.3: the dimension count

The dimension part of lem:flat-mesh-perturbations over a field: the identities ZH = I, ZH_B ≥ I, the bound H_B ≤ H and the matrix argument (see FlatPerturbation.lean).

theorem MultiplicativeBasisDeformations.FlatPert.finrank_alpha {k : Type u} [Field k] {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (J : IdealFam k V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] [∀ (w y : V), FiniteDimensional k (Q J w y)] (w x : V) : Module.finrank k (Q J w x) = Module.finrank k ↥(alpha J w x).range + if w = x then 1 else 0

The arrow map hits everything but the top: dim C(w, x) = rank α + δ_{wx}.

theorem MultiplicativeBasisDeformations.FlatPert.finrank_B_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)] (hN : ∀ (w y : V) (p : Quiver.Path w y), N ≤ p.length → LinearPaths.path p ∈ ctxSpan P P.r w y) (w y : V) : Module.finrank k (Q (idealB P f hf N) w y) ≤ Module.finrank k (Q (idealC P) w y)

H_B ≤ H.

The dimension matrices

theorem MultiplicativeBasisDeformations.FlatPert.matrix_arg {W : Type} [Fintype W] [DecidableEq W] (A R H HB : W → W → ℕ) (hC : ∀ (w x : W), ∑ y : W, R y x * H w y + H w x = ∑ y : W, A y x * H w y + if w = x then 1 else 0) (hB : ∀ (w x : W), (∑ y : W, A y x * HB w y + if w = x then 1 else 0) ≤ ∑ y : W, R y x * HB w y + HB w x) (hle : ∀ (w y : W), HB w y ≤ H w y) : HB = H ∧ ∀ (w x : W), (∑ y : W, A y x * HB w y + if w = x then 1 else 0) = ∑ y : W, R y x * HB w y + HB w x

The matrix argument (deformation-refinements.tex): ZH = I, ZH_B ≥ I and H_B ≤ H force H_B = H and ZH_B = I.

The dimension identities

theorem MultiplicativeBasisDeformations.FlatPert.sum_arrows {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)] (x : V) (h : V → ℕ) : ∑ a : (y : V) × (y ⟶ x), h a.fst = ∑ y : V, Fintype.card (y ⟶ x) * h y

theorem MultiplicativeBasisDeformations.FlatPert.sum_rels {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)] (x : V) (h : V → ℕ) : ∑ t : P.T x, h (P.src x t) = ∑ y : V, Fintype.card { t : P.T x // P.src x t = y } * h y

theorem MultiplicativeBasisDeformations.FlatPert.r_comp_mem_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)] (x : V) (t : P.T x) (w : V) (u : Hm k w (P.src x t)) : CategoryTheory.CategoryStruct.comp u (P.r x t) ∈ (idealC P).I w x

theorem MultiplicativeBasisDeformations.FlatPert.rf_comp_mem_B {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)] (x : V) (t : P.T x) (w : V) (u : Hm k w (P.src x t)) : CategoryTheory.CategoryStruct.comp u (rf P f x t) ∈ (idealB P f hf N).I w x

theorem MultiplicativeBasisDeformations.FlatPert.r_proj0 {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)] (x : V) (t : P.T x) : (LinearPaths.proj 0 (P.src x t) x) (P.r x t) = 0

theorem MultiplicativeBasisDeformations.FlatPert.dim_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))] (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) (w x : V) : ∑ t : P.T x, Module.finrank k (Q (idealC P) w (P.src x t)) + Module.finrank k (Q (idealC P) w x) = ∑ a : (y : V) × (y ⟶ x), Module.finrank k (Q (idealC P) w a.fst) + if w = x then 1 else 0

ZH = I from the assumed resolutions of C.

theorem MultiplicativeBasisDeformations.FlatPert.dim_B {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) (w x : V) : (∑ a : (y : V) × (y ⟶ x), Module.finrank k (Q (idealB P f hf N) w a.fst) + if w = x then 1 else 0) ≤ ∑ t : P.T x, Module.finrank k (Q (idealB P f hf N) w (P.src x t)) + Module.finrank k (Q (idealB P f hf N) w x)

ZH_B ≥ I from the exactness of the perturbed presentation at the arrow term.

Lemma 12.3

theorem MultiplicativeBasisDeformations.FlatPert.lift_basis_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)) (w y : V) {ι : Type} [Fintype ι] (p : ι → Quiver.Path w y) (hli : LinearIndependent k fun (i : ι) => Submodule.Quotient.mk (LinearPaths.path (p i))) (hsp : Submodule.span k (Set.range fun (i : ι) => Submodule.Quotient.mk (LinearPaths.path (p i))) = ⊤) : (LinearIndependent k fun (i : ι) => Submodule.Quotient.mk (LinearPaths.path (p i))) ∧ Submodule.span k (Set.range fun (i : ι) => Submodule.Quotient.mk (LinearPaths.path (p i))) = ⊤

A path basis of C lifts to a basis of B when B and C have the same dimensions.

theorem MultiplicativeBasisDeformations.FlatPert.flat_perturbation {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) : (∀ (w y : V), Module.finrank k (Q (idealB P f hf N) w y) = Module.finrank k (Q (idealC P) w y)) ∧ (∀ (w x : V), Function.Injective ⇑(relMap P (idealB P f hf N) (rf P f) w x) ∧ (alpha (idealB P f hf N) w x).ker ≤ (relMap P (idealB P f hf N) (rf P f) w x).range) ∧ ∀ (w y : V) {ι : Type} [Fintype ι] (p : ι → Quiver.Path w y), (LinearIndependent k fun (i : ι) => Submodule.Quotient.mk (LinearPaths.path (p i))) → Submodule.span k (Set.range fun (i : ι) => Submodule.Quotient.mk (LinearPaths.path (p i))) = ⊤ → (LinearIndependent k fun (i : ι) => Submodule.Quotient.mk (LinearPaths.path (p i))) ∧ Submodule.span k (Set.range fun (i : ι) => Submodule.Quotient.mk (LinearPaths.path (p i))) = ⊤

Lemma 12.3 (lem:flat-mesh-perturbations): if the presentations of the simple modules of C = kQ/(r) are resolutions and C_d = 0 for d ≥ N, then B = kQ/(𝔪^{N+1}, r − f) has the dimensions of C, its presentations are again resolutions, and every path basis of C lifts to a basis of B.