Lemma 12.3 for right modules and first arrows

lem:flat-mesh-perturbations is stated for right modules, splitting each relation by its first arrow; flat_perturbation uses the representables C(−, x) and last arrows. This file states the lemma in the manuscript's convention and derives it from the opposite quiver: path reversal gives isomorphisms kQ(w, y) ≅ kQᵒᵖ(y, w) reversing composition (opE), carrying the ideals of C and B to those of the opposite presentation, and the first-arrow presentations of the right simple modules to the last-arrow presentations of the representables of Qᵒᵖ.

Path reversal

@[irreducible]

def MultiplicativeBasisDeformations.FlatPert.pathOp {V : Type} [Quiver V] {x y : V} : Quiver.Path x y → Quiver.Path (Opposite.op y) (Opposite.op x)

The reversed path in the opposite quiver.

@[irreducible]

def MultiplicativeBasisDeformations.FlatPert.pathUnop {V : Type} [Quiver V] {a b : Vᵒᵖ} : Quiver.Path a b → Quiver.Path (Opposite.unop b) (Opposite.unop a)

The reversed path of a path of the opposite quiver.

@[simp]

theorem MultiplicativeBasisDeformations.FlatPert.pathOp_nil {V : Type} [Quiver V] (x : V) : pathOp Quiver.Path.nil = Quiver.Path.nil

theorem MultiplicativeBasisDeformations.FlatPert.pathOp_cons {V : Type} [Quiver V] {x y z : V} (p : Quiver.Path x y) (e : y ⟶ z) : pathOp (p.cons e) = e.op.toPath.comp (pathOp p)

@[simp]

theorem MultiplicativeBasisDeformations.FlatPert.pathUnop_nil {V : Type} [Quiver V] (a : Vᵒᵖ) : pathUnop Quiver.Path.nil = Quiver.Path.nil

theorem MultiplicativeBasisDeformations.FlatPert.pathUnop_cons {V : Type} [Quiver V] {a b c : Vᵒᵖ} (p : Quiver.Path a b) (e : b ⟶ c) : pathUnop (p.cons e) = e.unop.toPath.comp (pathUnop p)

theorem MultiplicativeBasisDeformations.FlatPert.pathOp_toPath {V : Type} [Quiver V] {x y : V} (e : x ⟶ y) : pathOp e.toPath = e.op.toPath

theorem MultiplicativeBasisDeformations.FlatPert.pathUnop_toPath {V : Type} [Quiver V] {a b : Vᵒᵖ} (e : a ⟶ b) : pathUnop e.toPath = e.unop.toPath

theorem MultiplicativeBasisDeformations.FlatPert.pathOp_comp {V : Type} [Quiver V] {x y : V} (p : Quiver.Path x y) {z : V} (q : Quiver.Path y z) : pathOp (p.comp q) = (pathOp q).comp (pathOp p)

theorem MultiplicativeBasisDeformations.FlatPert.pathUnop_comp {V : Type} [Quiver V] {a b : Vᵒᵖ} (p : Quiver.Path a b) {c : Vᵒᵖ} (q : Quiver.Path b c) : pathUnop (p.comp q) = (pathUnop q).comp (pathUnop p)

theorem MultiplicativeBasisDeformations.FlatPert.pathOp_length {V : Type} [Quiver V] {x y : V} (p : Quiver.Path x y) : (pathOp p).length = p.length

theorem MultiplicativeBasisDeformations.FlatPert.pathUnop_length {V : Type} [Quiver V] {a b : Vᵒᵖ} (p : Quiver.Path a b) : (pathUnop p).length = p.length

theorem MultiplicativeBasisDeformations.FlatPert.pathUnop_pathOp {V : Type} [Quiver V] {x y : V} (p : Quiver.Path x y) : pathUnop (pathOp p) = p

theorem MultiplicativeBasisDeformations.FlatPert.pathOp_pathUnop {V : Type} [Quiver V] {a b : Vᵒᵖ} (p : Quiver.Path a b) : pathOp (pathUnop p) = p

def MultiplicativeBasisDeformations.FlatPert.pathEquiv {V : Type} [Quiver V] (x y : V) : Quiver.Path x y ≃ Quiver.Path (Opposite.op y) (Opposite.op x)

Path reversal as an equivalence.

Reversal on kQ

noncomputable def MultiplicativeBasisDeformations.FlatPert.opE {V : Type} [Quiver V] {k : Type u} [Field k] (x y : V) : Hm k x y ≃ₗ[k] Hm k (Opposite.op y) (Opposite.op x)

Reversal kQ(x, y) ≅ kQᵒᵖ(op y, op x).

theorem MultiplicativeBasisDeformations.FlatPert.toFinsupp_opE {V : Type} [Quiver V] {k : Type u} [Field k] {x y : V} (g : Hm k x y) (q : Quiver.Path (Opposite.op y) (Opposite.op x)) : (LinearPaths.toFinsupp ((opE x y) g)) q = (LinearPaths.toFinsupp g) (pathUnop q)

theorem MultiplicativeBasisDeformations.FlatPert.opE_path {V : Type} [Quiver V] {k : Type u} [Field k] {x y : V} (p : Quiver.Path x y) : (opE x y) (LinearPaths.path p) = LinearPaths.path (pathOp p)

theorem MultiplicativeBasisDeformations.FlatPert.opE_comp {V : Type} [Quiver V] {k : Type u} [Field k] {x y z : V} (f : Hm k x y) (g : Hm k y z) : (opE x z) (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp ((opE y z) g) ((opE x y) f)

theorem MultiplicativeBasisDeformations.FlatPert.opE_comp3 {V : Type} [Quiver V] {k : Type u} [Field k] {w x z y : V} (u : Hm k w x) (r : Hm k x z) (v : Hm k z y) : (opE w y) (CategoryTheory.CategoryStruct.comp u (CategoryTheory.CategoryStruct.comp r v)) = CategoryTheory.CategoryStruct.comp ((opE z y) v) (CategoryTheory.CategoryStruct.comp ((opE x z) r) ((opE w x) u))

theorem MultiplicativeBasisDeformations.FlatPert.opE_id {V : Type} [Quiver V] {k : Type u} [Field k] (x : V) : (opE x x) (CategoryTheory.CategoryStruct.id (LinearPaths.obj x)) = CategoryTheory.CategoryStruct.id (LinearPaths.obj (Opposite.op x))

theorem MultiplicativeBasisDeformations.FlatPert.opE_arrow {V : Type} [Quiver V] {k : Type u} [Field k] {x y : V} (a : x ⟶ y) : (opE x y) (LinearPaths.arrow a) = LinearPaths.arrow a.op

theorem MultiplicativeBasisDeformations.FlatPert.map_opE_span {V : Type} [Quiver V] {k : Type u} [Field k] (S : ℕ → Prop) (x y : V) : Submodule.map (↑(opE x y)) (Submodule.span k {g : LinearPaths.obj x ⟶ LinearPaths.obj y | ∃ (p : Quiver.Path x y), S p.length ∧ g = LinearPaths.path p}) = Submodule.span k {g : LinearPaths.obj (Opposite.op y) ⟶ LinearPaths.obj (Opposite.op x) | ∃ (q : Quiver.Path (Opposite.op y) (Opposite.op x)), S q.length ∧ g = LinearPaths.path q}

theorem MultiplicativeBasisDeformations.FlatPert.map_opE_geSpan {V : Type} [Quiver V] {k : Type u} [Field k] (d : ℕ) (x y : V) : Submodule.map (↑(opE x y)) (geSpan k d x y) = geSpan k d (Opposite.op y) (Opposite.op x)

theorem MultiplicativeBasisDeformations.FlatPert.map_opE_degreePart {V : Type} [Quiver V] {k : Type u} [Field k] (d : ℕ) (x y : V) : Submodule.map (↑(opE x y)) (LinearPaths.degreePart d x y) = LinearPaths.degreePart d (Opposite.op y) (Opposite.op x)

theorem MultiplicativeBasisDeformations.FlatPert.opE_mem_degreePart {V : Type} [Quiver V] {k : Type u} [Field k] {d : ℕ} {x y : V} {g : Hm k x y} (hg : g ∈ LinearPaths.degreePart d x y) : (opE x y) g ∈ LinearPaths.degreePart d (Opposite.op y) (Opposite.op x)

theorem MultiplicativeBasisDeformations.FlatPert.opE_mem_geSpan {V : Type} [Quiver V] {k : Type u} [Field k] {d : ℕ} {x y : V} {g : Hm k x y} (hg : g ∈ geSpan k d x y) : (opE x y) g ∈ geSpan k d (Opposite.op y) (Opposite.op x)

def MultiplicativeBasisDeformations.FlatPert.arrowsOp {V : Type} [Quiver V] (x : V) : (y : V) × (x ⟶ y) ≃ (b : Vᵒᵖ) × (b ⟶ Opposite.op x)

The arrows out of x and the arrows into op x.

@[instance_reducible]

instance MultiplicativeBasisDeformations.FlatPert.instFintypeOpposite_multiplicativeBasisDeformations {V : Type} [Fintype V] : Fintype Vᵒᵖ

@[instance_reducible]

instance MultiplicativeBasisDeformations.FlatPert.instFintypeHomOpposite_multiplicativeBasisDeformations {V : Type} [Quiver V] [(x y : V) → Fintype (x ⟶ y)] (a b : Vᵒᵖ) : Fintype (a ⟶ b)

Presentations by an indexed family of relations

structure MultiplicativeBasisDeformations.FlatPert.PresI (k : Type u) [Field k] (V : Type) [Quiver V] : Type (max 1 u)

A graded presentation C = kQ/(r₁, …, r_t) with relations r_i : s_i → t_i, homogeneous of degree at least two.

• ι : Type
• fin : Fintype self.ι
• s : self.ι → V
• t : self.ι → V
• deg : self.ι → ℕ
• r (i : self.ι) : Hm k (self.s i) (self.t i)
• hom (i : self.ι) : self.r i ∈ LinearPaths.degreePart (self.deg i) (self.s i) (self.t i)
• two (i : self.ι) : 2 ≤ self.deg i

@[instance_reducible]

instance MultiplicativeBasisDeformations.FlatPert.instDecidableEqOpposite_multiplicativeBasisDeformations {V : Type} [DecidableEq V] : DecidableEq Vᵒᵖ

@[instance_reducible]

instance MultiplicativeBasisDeformations.FlatPert.instDecidableEqHomOpposite_multiplicativeBasisDeformations {V : Type} [Quiver V] [(x y : V) → DecidableEq (x ⟶ y)] (a b : Vᵒᵖ) : DecidableEq (a ⟶ b)

noncomputable def MultiplicativeBasisDeformations.FlatPert.PresI.famT {V : Type} [Quiver V] {k : Type u} [Field k] (P : PresI k V) (ρ : (i : P.ι) → Hm k (P.s i) (P.t i)) (y : V) (j : { i : P.ι // P.t i = y }) : Hm k (P.s ↑j) y

A family of maps parallel to the relations, indexed by targets.

noncomputable def MultiplicativeBasisDeformations.FlatPert.PresI.famO {V : Type} [Quiver V] {k : Type u} [Field k] (P : PresI k V) (ρ : (i : P.ι) → Hm k (P.s i) (P.t i)) (a : Vᵒᵖ) (j : { i : P.ι // P.s i = Opposite.unop a }) : Hm k (Opposite.op (P.t ↑j)) a

A family of maps parallel to the relations, reversed and indexed by sources.

@[simp]

theorem MultiplicativeBasisDeformations.FlatPert.PresI.famT_self {V : Type} [Quiver V] {k : Type u} [Field k] [Fintype V] [(x y : V) → Fintype (x ⟶ y)] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (P : PresI k V) (ρ : (i : P.ι) → Hm k (P.s i) (P.t i)) (i : P.ι) : P.famT ρ (P.t i) ⟨i, ⋯⟩ = ρ i

@[simp]

theorem MultiplicativeBasisDeformations.FlatPert.PresI.famO_self {V : Type} [Quiver V] {k : Type u} [Field k] [Fintype V] [(x y : V) → Fintype (x ⟶ y)] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (P : PresI k V) (ρ : (i : P.ι) → Hm k (P.s i) (P.t i)) (i : P.ι) : P.famO ρ (Opposite.op (P.s i)) ⟨i, ⋯⟩ = (opE (P.s i) (P.t i)) (ρ i)

noncomputable def MultiplicativeBasisDeformations.FlatPert.PresI.toPres {V : Type} [Quiver V] {k : Type u} [Field k] [Fintype V] [(x y : V) → Fintype (x ⟶ y)] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (P : PresI k V) : Pres k V

The presentation indexed by targets.

noncomputable def MultiplicativeBasisDeformations.FlatPert.PresI.opPres {V : Type} [Quiver V] {k : Type u} [Field k] [Fintype V] [(x y : V) → Fintype (x ⟶ y)] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (P : PresI k V) : Pres k Vᵒᵖ

The opposite presentation on Qᵒᵖ, indexed by the sources of the relations.

theorem MultiplicativeBasisDeformations.FlatPert.PresI.ctx_mem_T {V : Type} [Quiver V] {k : Type u} [Field k] [Fintype V] [(x y : V) → Fintype (x ⟶ y)] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (P : PresI k V) (ρ : (i : P.ι) → Hm k (P.s i) (P.t i)) (i : P.ι) {w y : V} (u : Hm k w (P.s i)) (v : Hm k (P.t i) y) : CategoryTheory.CategoryStruct.comp u (CategoryTheory.CategoryStruct.comp (ρ i) v) ∈ ctxSpan P.toPres (P.famT ρ) w y

theorem MultiplicativeBasisDeformations.FlatPert.PresI.ctx_mem_O {V : Type} [Quiver V] {k : Type u} [Field k] [Fintype V] [(x y : V) → Fintype (x ⟶ y)] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (P : PresI k V) (ρ : (i : P.ι) → Hm k (P.s i) (P.t i)) (i : P.ι) {a b : Vᵒᵖ} (u : Hm k a (Opposite.op (P.t i))) (v : Hm k (Opposite.op (P.s i)) b) : CategoryTheory.CategoryStruct.comp u (CategoryTheory.CategoryStruct.comp ((opE (P.s i) (P.t i)) (ρ i)) v) ∈ ctxSpan P.opPres (P.famO ρ) a b

theorem MultiplicativeBasisDeformations.FlatPert.PresI.map_ctx {V : Type} [Quiver V] {k : Type u} [Field k] [Fintype V] [(x y : V) → Fintype (x ⟶ y)] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (P : PresI k V) (ρ : (i : P.ι) → Hm k (P.s i) (P.t i)) (w y : V) : Submodule.map (↑(opE w y)) (ctxSpan P.toPres (P.famT ρ) w y) = ctxSpan P.opPres (P.famO ρ) (Opposite.op y) (Opposite.op w)

theorem MultiplicativeBasisDeformations.FlatPert.PresI.famT_sub {V : Type} [Quiver V] {k : Type u} [Field k] [Fintype V] [(x y : V) → Fintype (x ⟶ y)] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (P : PresI k V) (ρ σ : (i : P.ι) → Hm k (P.s i) (P.t i)) : (fun (y : V) (j : { i : P.ι // P.t i = y }) => P.famT ρ y j - P.famT σ y j) = P.famT fun (i : P.ι) => ρ i - σ i

theorem MultiplicativeBasisDeformations.FlatPert.PresI.famO_sub {V : Type} [Quiver V] {k : Type u} [Field k] [Fintype V] [(x y : V) → Fintype (x ⟶ y)] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (P : PresI k V) (ρ σ : (i : P.ι) → Hm k (P.s i) (P.t i)) : (fun (a : Vᵒᵖ) (j : { i : P.ι // P.s i = Opposite.unop a }) => P.famO ρ a j - P.famO σ a j) = P.famO fun (i : P.ι) => ρ i - σ i

theorem MultiplicativeBasisDeformations.FlatPert.PresI.map_C {V : Type} [Quiver V] {k : Type u} [Field k] [Fintype V] [(x y : V) → Fintype (x ⟶ y)] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (P : PresI k V) (w y : V) : Submodule.map (↑(opE w y)) ((idealC P.toPres).I w y) = (idealC P.opPres).I (Opposite.op y) (Opposite.op w)

theorem MultiplicativeBasisDeformations.FlatPert.PresI.hfT {V : Type} [Quiver V] {k : Type u} [Field k] [Fintype V] [(x y : V) → Fintype (x ⟶ y)] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (P : PresI k V) (f : (i : P.ι) → Hm k (P.s i) (P.t i)) (hf : ∀ (i : P.ι), f i ∈ geSpan k (P.deg i + 1) (P.s i) (P.t i)) (y : V) (j : P.toPres.T y) : P.famT f y j ∈ geSpan k (P.toPres.deg y j + 1) (P.toPres.src y j) y

theorem MultiplicativeBasisDeformations.FlatPert.PresI.hfO {V : Type} [Quiver V] {k : Type u} [Field k] [Fintype V] [(x y : V) → Fintype (x ⟶ y)] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (P : PresI k V) (f : (i : P.ι) → Hm k (P.s i) (P.t i)) (hf : ∀ (i : P.ι), f i ∈ geSpan k (P.deg i + 1) (P.s i) (P.t i)) (a : Vᵒᵖ) (j : P.opPres.T a) : P.famO f a j ∈ geSpan k (P.opPres.deg a j + 1) (P.opPres.src a j) a

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.FlatPert.PresI.idealBT {V : Type} [Quiver V] {k : Type u} [Field k] [Fintype V] [(x y : V) → Fintype (x ⟶ y)] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (P : PresI k V) (f : (i : P.ι) → Hm k (P.s i) (P.t i)) (hf : ∀ (i : P.ι), f i ∈ geSpan k (P.deg i + 1) (P.s i) (P.t i)) (N : ℕ) : IdealFam k V

The ideal of B = kQ/(𝔪^{N+1}, r_i − f_i).

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.FlatPert.PresI.idealBO {V : Type} [Quiver V] {k : Type u} [Field k] [Fintype V] [(x y : V) → Fintype (x ⟶ y)] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (P : PresI k V) (f : (i : P.ι) → Hm k (P.s i) (P.t i)) (hf : ∀ (i : P.ι), f i ∈ geSpan k (P.deg i + 1) (P.s i) (P.t i)) (N : ℕ) : IdealFam k Vᵒᵖ

The ideal of the opposite of B.

theorem MultiplicativeBasisDeformations.FlatPert.PresI.map_B {V : Type} [Quiver V] {k : Type u} [Field k] [Fintype V] [(x y : V) → Fintype (x ⟶ y)] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (P : PresI k V) (f : (i : P.ι) → Hm k (P.s i) (P.t i)) (hf : ∀ (i : P.ι), f i ∈ geSpan k (P.deg i + 1) (P.s i) (P.t i)) (N : ℕ) (w y : V) : Submodule.map (↑(opE w y)) ((P.idealBT f hf N).I w y) = (P.idealBO f hf N).I (Opposite.op y) (Opposite.op w)

Transport of quotients

noncomputable def MultiplicativeBasisDeformations.FlatPert.qE {V : Type} [Quiver V] {k : Type u} [Field k] (J : IdealFam k V) (J' : IdealFam k Vᵒᵖ) (hJ : ∀ (w y : V), Submodule.map (↑(opE w y)) (J.I w y) = J'.I (Opposite.op y) (Opposite.op w)) (y w : V) : Q J y w ≃ₗ[k] Q J' (Opposite.op w) (Opposite.op y)

Reversal on the quotients (kQ/J)(y, w) ≅ (kQᵒᵖ/J')(op w, op y).

theorem MultiplicativeBasisDeformations.FlatPert.qE_mk {V : Type} [Quiver V] {k : Type u} [Field k] [Fintype V] [(x y : V) → Fintype (x ⟶ y)] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (J : IdealFam k V) (J' : IdealFam k Vᵒᵖ) (hJ : ∀ (w y : V), Submodule.map (↑(opE w y)) (J.I w y) = J'.I (Opposite.op y) (Opposite.op w)) {y w : V} (g : Hm k y w) : (qE J J' hJ y w) (Submodule.Quotient.mk g) = Submodule.Quotient.mk ((opE y w) g)

theorem MultiplicativeBasisDeformations.FlatPert.finrank_qE {V : Type} [Quiver V] {k : Type u} [Field k] [Fintype V] [(x y : V) → Fintype (x ⟶ y)] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (J : IdealFam k V) (J' : IdealFam k Vᵒᵖ) (hJ : ∀ (w y : V), Submodule.map (↑(opE w y)) (J.I w y) = J'.I (Opposite.op y) (Opposite.op w)) (y w : V) : Module.finrank k (Q J y w) = Module.finrank k (Q J' (Opposite.op w) (Opposite.op y))

noncomputable def MultiplicativeBasisDeformations.FlatPert.compL {V : Type} [Quiver V] {k : Type u} [Field k] {x y w : V} (h : Hm k x y) : Hm k y w →ₗ[k] Hm k x w

Left composition with a morphism of kQ.

noncomputable def MultiplicativeBasisDeformations.FlatPert.compQL {V : Type} [Quiver V] {k : Type u} [Field k] (J : IdealFam k V) {x y w : V} (h : Hm k x y) : Q J y w →ₗ[k] Q J x w

Left composition on the quotients.

theorem MultiplicativeBasisDeformations.FlatPert.compQL_mk {V : Type} [Quiver V] {k : Type u} [Field k] [Fintype V] [(x y : V) → Fintype (x ⟶ y)] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (J : IdealFam k V) {x y w : V} (h : Hm k x y) (g : Hm k y w) : (compQL J h) (Submodule.Quotient.mk g) = Submodule.Quotient.mk (CategoryTheory.CategoryStruct.comp h g)

theorem MultiplicativeBasisDeformations.FlatPert.qE_compQL {V : Type} [Quiver V] {k : Type u} [Field k] [Fintype V] [(x y : V) → Fintype (x ⟶ y)] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (J : IdealFam k V) (J' : IdealFam k Vᵒᵖ) (hJ : ∀ (w y : V), Submodule.map (↑(opE w y)) (J.I w y) = J'.I (Opposite.op y) (Opposite.op w)) {x y w : V} (h : Hm k x y) (q : Q J y w) : (qE J J' hJ x w) ((compQL J h) q) = (compQ J' ((opE x y) h)) ((qE J J' hJ y w) q)

First-arrow components

theorem MultiplicativeBasisDeformations.FlatPert.toPath_comp_injective {V : Type} [Quiver V] [Fintype V] [(x y : V) → Fintype (x ⟶ y)] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] {x y z : V} (a : x ⟶ y) : Function.Injective fun (p : Quiver.Path y z) => a.toPath.comp p

noncomputable def MultiplicativeBasisDeformations.FlatPert.firstComp {V : Type} [Quiver V] {k : Type u} [Field k] [Fintype V] [(x y : V) → Fintype (x ⟶ y)] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] {x z : V} (a : (y : V) × (x ⟶ y)) : Hm k x z →ₗ[k] Hm k a.fst z

The first-arrow components f = f₀ + Σ_a a f_a.

theorem MultiplicativeBasisDeformations.FlatPert.toFinsupp_firstComp {V : Type} [Quiver V] {k : Type u} [Field k] [Fintype V] [(x y : V) → Fintype (x ⟶ y)] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] {x z : V} (a : (y : V) × (x ⟶ y)) (g : Hm k x z) (p : Quiver.Path a.fst z) : (LinearPaths.toFinsupp ((firstComp a) g)) p = (LinearPaths.toFinsupp g) (a.snd.toPath.comp p)

theorem MultiplicativeBasisDeformations.FlatPert.lastComp_opE {V : Type} [Quiver V] {k : Type u} [Field k] [Fintype V] [(x y : V) → Fintype (x ⟶ y)] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] {x z : V} (a : (y : V) × (x ⟶ y)) (g : Hm k x z) : (lastComp ((arrowsOp x) a)) ((opE x z) g) = (opE a.fst z) ((firstComp a) g)

The first-arrow presentations of the right simple modules

noncomputable def MultiplicativeBasisDeformations.FlatPert.PresI.famS {V : Type} [Quiver V] {k : Type u} [Field k] (P : PresI k V) (ρ : (i : P.ι) → Hm k (P.s i) (P.t i)) (x : V) (i : { i : P.ι // P.s i = x }) : Hm k x (P.t ↑i)

The relations starting at x, as maps out of x.

theorem MultiplicativeBasisDeformations.FlatPert.PresI.famO_op {V : Type} [Quiver V] {k : Type u} [Field k] [Fintype V] [(x y : V) → Fintype (x ⟶ y)] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (P : PresI k V) (ρ : (i : P.ι) → Hm k (P.s i) (P.t i)) (x : V) (i : { i : P.ι // P.s i = x }) : P.famO ρ (Opposite.op x) i = (opE x (P.t ↑i)) (P.famS ρ x i)

noncomputable def MultiplicativeBasisDeformations.FlatPert.alphaR {V : Type} [Quiver V] {k : Type u} [Field k] [Fintype V] [(x y : V) → Fintype (x ⟶ y)] (J : IdealFam k V) (w x : V) : ((a : (y : V) × (x ⟶ y)) → Q J a.fst w) →ₗ[k] Q J x w

The arrow map of the right simple module S_x, evaluated at w: ⊕_{a : x → y} B(y, w) → B(x, w), (z_a) ↦ Σ_a a z_a.

noncomputable def MultiplicativeBasisDeformations.FlatPert.relMapR {V : Type} [Quiver V] {k : Type u} [Field k] [Fintype V] [(x y : V) → Fintype (x ⟶ y)] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (P : PresI k V) (J : IdealFam k V) (ρ : (i : P.ι) → Hm k (P.s i) (P.t i)) (w x : V) : ((i : { i : P.ι // P.s i = x }) → Q J (P.t ↑i) w) →ₗ[k] (a : (y : V) × (x ⟶ y)) → Q J a.fst w

The relation map ⊕_{r_i : x → t_i} B(t_i, w) → ⊕_{a : x → y} B(y, w), splitting each relation starting at x by its first arrows.

noncomputable def MultiplicativeBasisDeformations.FlatPert.piA {V : Type} [Quiver V] {k : Type u} [Field k] (J : IdealFam k V) (J' : IdealFam k Vᵒᵖ) (hJ : ∀ (w y : V), Submodule.map (↑(opE w y)) (J.I w y) = J'.I (Opposite.op y) (Opposite.op w)) (w x : V) : ((a : (y : V) × (x ⟶ y)) → Q J a.fst w) ≃ₗ[k] (b : (b : Vᵒᵖ) × (b ⟶ Opposite.op x)) → Q J' (Opposite.op w) b.fst

The arrow terms, reversed.

noncomputable def MultiplicativeBasisDeformations.FlatPert.piR {V : Type} [Quiver V] {k : Type u} [Field k] [Fintype V] [(x y : V) → Fintype (x ⟶ y)] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (P : PresI k V) (J : IdealFam k V) (J' : IdealFam k Vᵒᵖ) (hJ : ∀ (w y : V), Submodule.map (↑(opE w y)) (J.I w y) = J'.I (Opposite.op y) (Opposite.op w)) (w x : V) : ((i : { i : P.ι // P.s i = x }) → Q J (P.t ↑i) w) ≃ₗ[k] (j : P.opPres.T (Opposite.op x)) → Q J' (Opposite.op w) (P.opPres.src (Opposite.op x) j)

The relation terms, reversed.

theorem MultiplicativeBasisDeformations.FlatPert.piA_apply {V : Type} [Quiver V] {k : Type u} [Field k] [Fintype V] [(x y : V) → Fintype (x ⟶ y)] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (J : IdealFam k V) (J' : IdealFam k Vᵒᵖ) (hJ : ∀ (w y : V), Submodule.map (↑(opE w y)) (J.I w y) = J'.I (Opposite.op y) (Opposite.op w)) (w x : V) (c : (a : (y : V) × (x ⟶ y)) → Q J a.fst w) (a : (y : V) × (x ⟶ y)) : (piA J J' hJ w x) c ((arrowsOp x) a) = (qE J J' hJ a.fst w) (c a)

theorem MultiplicativeBasisDeformations.FlatPert.piR_apply {V : Type} [Quiver V] {k : Type u} [Field k] [Fintype V] [(x y : V) → Fintype (x ⟶ y)] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (P : PresI k V) (J : IdealFam k V) (J' : IdealFam k Vᵒᵖ) (hJ : ∀ (w y : V), Submodule.map (↑(opE w y)) (J.I w y) = J'.I (Opposite.op y) (Opposite.op w)) (w x : V) (d : (i : { i : P.ι // P.s i = x }) → Q J (P.t ↑i) w) (i : { i : P.ι // P.s i = x }) : (piR P J J' hJ w x) d i = (qE J J' hJ (P.t ↑i) w) (d i)

theorem MultiplicativeBasisDeformations.FlatPert.alpha_piA {V : Type} [Quiver V] {k : Type u} [Field k] [Fintype V] [(x y : V) → Fintype (x ⟶ y)] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (J : IdealFam k V) (J' : IdealFam k Vᵒᵖ) (hJ : ∀ (w y : V), Submodule.map (↑(opE w y)) (J.I w y) = J'.I (Opposite.op y) (Opposite.op w)) (w x : V) (c : (a : (y : V) × (x ⟶ y)) → Q J a.fst w) : (alpha J' (Opposite.op w) (Opposite.op x)) ((piA J J' hJ w x) c) = (qE J J' hJ x w) ((alphaR J w x) c)

theorem MultiplicativeBasisDeformations.FlatPert.relMap_piR {V : Type} [Quiver V] {k : Type u} [Field k] [Fintype V] [(x y : V) → Fintype (x ⟶ y)] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (P : PresI k V) (J : IdealFam k V) (J' : IdealFam k Vᵒᵖ) (hJ : ∀ (w y : V), Submodule.map (↑(opE w y)) (J.I w y) = J'.I (Opposite.op y) (Opposite.op w)) (ρ : (i : P.ι) → Hm k (P.s i) (P.t i)) (w x : V) (d : (i : { i : P.ι // P.s i = x }) → Q J (P.t ↑i) w) : (relMap P.opPres J' (P.famO ρ) (Opposite.op w) (Opposite.op x)) ((piR P J J' hJ w x) d) = (piA J J' hJ w x) ((relMapR P J ρ w x) d)

theorem MultiplicativeBasisDeformations.FlatPert.injective_relMapR_iff {V : Type} [Quiver V] {k : Type u} [Field k] [Fintype V] [(x y : V) → Fintype (x ⟶ y)] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (P : PresI k V) (J : IdealFam k V) (J' : IdealFam k Vᵒᵖ) (hJ : ∀ (w y : V), Submodule.map (↑(opE w y)) (J.I w y) = J'.I (Opposite.op y) (Opposite.op w)) (ρ : (i : P.ι) → Hm k (P.s i) (P.t i)) (w x : V) : Function.Injective ⇑(relMapR P J ρ w x) ↔ Function.Injective ⇑(relMap P.opPres J' (P.famO ρ) (Opposite.op w) (Opposite.op x))

theorem MultiplicativeBasisDeformations.FlatPert.ker_le_range_iff {V : Type} [Quiver V] {k : Type u} [Field k] [Fintype V] [(x y : V) → Fintype (x ⟶ y)] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (P : PresI k V) (J : IdealFam k V) (J' : IdealFam k Vᵒᵖ) (hJ : ∀ (w y : V), Submodule.map (↑(opE w y)) (J.I w y) = J'.I (Opposite.op y) (Opposite.op w)) (ρ : (i : P.ι) → Hm k (P.s i) (P.t i)) (w x : V) : (alphaR J w x).ker ≤ (relMapR P J ρ w x).range ↔ (alpha J' (Opposite.op w) (Opposite.op x)).ker ≤ (relMap P.opPres J' (P.famO ρ) (Opposite.op w) (Opposite.op x)).range

Lemma 12.3

theorem MultiplicativeBasisDeformations.FlatPert.flat_perturbation_right {V : Type} [Quiver V] {k : Type u} [Field k] [Fintype V] [(x y : V) → Fintype (x ⟶ y)] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (P : PresI k V) (f : (i : P.ι) → Hm k (P.s i) (P.t i)) (hf : ∀ (i : P.ι), f i ∈ geSpan k (P.deg i + 1) (P.s i) (P.t i)) (N : ℕ) (hN : ∀ (w y : V) (p : Quiver.Path w y), N ≤ p.length → LinearPaths.path p ∈ (idealC P.toPres).I w y) (hC : ∀ (w x : V), Function.Injective ⇑(relMapR P (idealC P.toPres) P.r w x) ∧ (alphaR (idealC P.toPres) w x).ker ≤ (relMapR P (idealC P.toPres) P.r w x).range) : (∀ (d : ℕ) (w y : V), ∃ (e : ↥(CD P.toPres d w y) ≃ₗ[k] grB P.toPres (P.famT f) ⋯ N d w y), ∀ (g : ↥(LinearPaths.degreePart d w y)), e ⟨(ψC P.toPres d w y) g, ⋯⟩ = (θ₀ P.toPres (P.famT f) ⋯ N d w y) g) ∧ (∀ (w y : V), Module.finrank k (Q (P.idealBT f hf N) w y) = Module.finrank k (Q (idealC P.toPres) w y)) ∧ (∀ (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))) = ⊤) ∧ ∀ (w x : V), Function.Injective ⇑(relMapR P (P.idealBT f hf N) (fun (i : P.ι) => P.r i - f i) w x) ∧ (alphaR (P.idealBT f hf N) w x).ker ≤ (relMapR P (P.idealBT f hf N) (fun (i : P.ι) => P.r i - f i) w x).range

Lemma 12.3 (lem:flat-mesh-perturbations), in the source's convention: let C = kQ/(r₁, …, r_t) be a graded presentation with relations of degree at least two such that the presentations of the right simple modules obtained by splitting each relation by its first arrow are projective resolutions of length at most two (hC: at every w, the relation map is injective and its image is the kernel of the arrow map), let C_d = 0 for d ≥ N (hN) and let f_i be parallel to r_i of strictly higher degree. Then B = kQ/(𝔪^{N+1}, r_i − f_i) has gr_𝔪 B ≅ C (in every degree d, paths induce C_d(w, y) ≅ 𝔪^d B(w, y)/𝔪^{d+1} B(w, y)), the dimensions of C, every path basis of C lifts to a basis of B, and splitting the perturbed relations by their first arrows gives projective resolutions of the right simple modules of B.