Multiplicative bases

MultiplicativeBasisDeformations.Refinements.FlatPerturbation

Lemma 12.3: flat mesh perturbations #

deformation-refinements.tex (lem:flat-mesh-perturbations). Let C = kQ/(r₁, …, r_t) be finite-dimensional and graded, with homogeneous relations of degree at least two, and assume that the presentations of the simple modules obtained by splitting each relation according to its arrows are projective resolutions of length at most two. Choose N with C_d = 0 for d ≥ N and perturbations f_i of strictly higher degree, and put B = kQ/(𝔪^{N+1}, r₁ − f₁, …, r_t − f_t). Then B has the dimensions of C, every homogeneous path basis of C lifts to a basis of B, and the perturbed presentations are again resolutions.

The proof is the source's: exactness of the perturbed presentations at the arrow term (contextual relations are sorted by their last factor), the dimension identities ZH = I and ZH_B = I + K, and the spanning bound H_B ≤ H.

Conventions. The source uses right modules and splits relations by their first arrow; we use the representables C(−, x) and split relations by their last arrow, the form in which the mesh relations and their exact sequences appear in Section 2 (the lemma for one convention is the lemma for the opposite quiver in the other). Relations are indexed by their target.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.FlatPert.Hm (k : Type u) [CommRing k] {V : Type} [Quiver V] (x y : V) :

The morphisms x → y of the linear path category kQ.

Instances For

theorem MultiplicativeBasisDeformations.FlatPert.path_comp_arrow {k : Type u} [CommRing k] {V : Type} [Quiver V] {x y z : V} (p : Quiver.Path x y) (a : y ⟶ z) :

CategoryTheory.CategoryStruct.comp (LinearPaths.path p) (LinearPaths.arrow a) = LinearPaths.path (p.cons a)

theorem MultiplicativeBasisDeformations.FlatPert.comp_arrow {k : Type u} [CommRing k] {V : Type} [Quiver V] {x y z : V} (g : Hm k x y) (a : y ⟶ z) :

CategoryTheory.CategoryStruct.comp g (LinearPaths.arrow a) = LinearPaths.ofFinsupp (Finsupp.mapDomain (fun (p : Quiver.Path x y) => p.cons a) (LinearPaths.toFinsupp g))

Composition with an arrow is mapDomain along · .cons a.

theorem MultiplicativeBasisDeformations.FlatPert.cons_injective {V : Type} [Quiver V] {x y z : V} (a : y ⟶ z) :

Function.Injective fun (p : Quiver.Path x y) => p.cons a

noncomputable def MultiplicativeBasisDeformations.FlatPert.lastComp {k : Type u} [CommRing k] {V : Type} [Quiver V] {x z : V} (a : (y : V) × (y ⟶ z)) :

Hm k x z →ₗ[k] Hm k x a.fst

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

Instances For

theorem MultiplicativeBasisDeformations.FlatPert.lastComp_apply {k : Type u} [CommRing k] {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] {x z : V} (a : (y : V) × (y ⟶ z)) (f : Hm k x z) (p : Quiver.Path x a.fst) :

(LinearPaths.toFinsupp ((lastComp a) f)) p = (LinearPaths.toFinsupp f) (p.cons a.snd)

theorem MultiplicativeBasisDeformations.FlatPert.lastComp_comp_arrow {k : Type u} [CommRing k] {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] {x y z : V} (g : Hm k x y) (b : y ⟶ z) :

(fun (a : (y : V) × (y ⟶ z)) => (lastComp a) (CategoryTheory.CategoryStruct.comp g (LinearPaths.arrow b))) = Pi.single ⟨y, b⟩ g

The components of g a: only the component of a survives.

theorem MultiplicativeBasisDeformations.FlatPert.decomp {k : Type u} [CommRing k] {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] {x z : V} [Fintype ((y : V) × (y ⟶ z))] (f : Hm k x z) :

f = (LinearPaths.proj 0 x z) f + ∑ a : (y : V) × (y ⟶ z), CategoryTheory.CategoryStruct.comp ((lastComp a) f) (LinearPaths.arrow a.snd)

The last-arrow decomposition f = f₀ + Σ_a f_a a.

theorem MultiplicativeBasisDeformations.FlatPert.lastComp_comp {k : Type u} [CommRing k] {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] {x y z : V} [Fintype ((y : V) × (y ⟶ z))] (g : Hm k x y) (h : Hm k y z) (h0 : (LinearPaths.proj 0 y z) h = 0) (a : (y : V) × (y ⟶ z)) :

(lastComp a) (CategoryTheory.CategoryStruct.comp g h) = CategoryTheory.CategoryStruct.comp g ((lastComp a) h)

Components of a composite with a morphism without degree-zero part.

noncomputable def MultiplicativeBasisDeformations.FlatPert.compR {k : Type u} [CommRing k] {V : Type} [Quiver V] {x y z : V} (h : Hm k y z) :

Hm k x y →ₗ[k] Hm k x z

Right composition as a linear map.

Instances For

@[simp]

theorem MultiplicativeBasisDeformations.FlatPert.compR_apply {k : Type u} [CommRing k] {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] {x y z : V} (h : Hm k y z) (g : Hm k x y) :

(compR h) g = CategoryTheory.CategoryStruct.comp g h

theorem MultiplicativeBasisDeformations.FlatPert.path_nil {k : Type u} [CommRing k] {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (x : V) :

LinearPaths.path Quiver.Path.nil = CategoryTheory.CategoryStruct.id (LinearPaths.obj x)

Paths of large length #

noncomputable def MultiplicativeBasisDeformations.FlatPert.geSpan (k : Type u) [CommRing k] {V : Type} [Quiver V] (d : ℕ) (x y : V) :

Submodule k (Hm k x y)

The span of the paths of length at least d (the power 𝔪^d of the arrow ideal).

Instances For

theorem MultiplicativeBasisDeformations.FlatPert.geSpan_anti {k : Type u} [CommRing k] {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] {d d' : ℕ} (h : d ≤ d') (x y : V) :

geSpan k d' x y ≤ geSpan k d x y

theorem MultiplicativeBasisDeformations.FlatPert.path_comp_geSpan {k : Type u} [CommRing k] {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] {d : ℕ} {w x y z : V} (u : Quiver.Path w x) (v : Quiver.Path y z) {g : Hm k x y} (hg : g ∈ geSpan k d x y) :

CategoryTheory.CategoryStruct.comp (LinearPaths.path u) (CategoryTheory.CategoryStruct.comp g (LinearPaths.path v)) ∈ geSpan k (u.length + d + v.length) w z

theorem MultiplicativeBasisDeformations.FlatPert.degreePart_le_geSpan {k : Type u} [CommRing k] {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (d : ℕ) (x y : V) :

LinearPaths.degreePart d x y ≤ geSpan k d x y

theorem MultiplicativeBasisDeformations.FlatPert.comp_geSpan {k : Type u} [CommRing k] {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] {d e : ℕ} {x y z : V} {g : Hm k x y} {h : Hm k y z} (hg : g ∈ geSpan k d x y) (hh : h ∈ geSpan k e y z) :

CategoryTheory.CategoryStruct.comp g h ∈ geSpan k (d + e) x z

noncomputable def MultiplicativeBasisDeformations.FlatPert.nilCoeff {k : Type u} [CommRing k] {V : Type} [Quiver V] (x : V) :

Hm k x x →ₗ[k] k

The nil coefficient of an endomorphism.

Instances For

theorem MultiplicativeBasisDeformations.FlatPert.nilCoeff_geSpan {k : Type u} [CommRing k] {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] {x : V} {g : Hm k x x} (hg : g ∈ geSpan k 1 x x) :

(nilCoeff x) g = 0

theorem MultiplicativeBasisDeformations.FlatPert.nilCoeff_id {k : Type u} [CommRing k] {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (x : V) :

(nilCoeff x) (CategoryTheory.CategoryStruct.id (LinearPaths.obj x)) = 1

theorem MultiplicativeBasisDeformations.FlatPert.mem_geSpan_zero {k : Type u} [CommRing k] {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] {x y : V} (g : Hm k x y) :

g ∈ geSpan k 0 x y

Presentations and their ideals #

structure MultiplicativeBasisDeformations.FlatPert.Pres (k : Type u) [CommRing k] (V : Type) [Quiver V] :

Type (max 1 u)

A graded presentation kQ/(r): relations indexed by their target, homogeneous of degree at least two.

T : V → Type
fin (x : V) : Fintype (self.T x)
src (x : V) : self.T x → V
deg (x : V) : self.T x → ℕ
r (x : V) (t : self.T x) : Hm k (self.src x t) x
hom (x : V) (t : self.T x) : self.r x t ∈ LinearPaths.degreePart (self.deg x t) (self.src x t) x
two (x : V) (t : self.T x) : 2 ≤ self.deg x t

Instances For

noncomputable def MultiplicativeBasisDeformations.FlatPert.ctxSpan {k : Type u} [CommRing k] {V : Type} [Quiver V] (P : Pres k V) (ρ : (x : V) → (t : P.T x) → Hm k (P.src x t) x) (w y : V) :

Submodule k (Hm k w y)

The span of the contextual relations u ρ_t v.

Instances For

theorem MultiplicativeBasisDeformations.FlatPert.ctx_mem {k : Type u} [CommRing k] {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (P : Pres k V) (ρ : (x : V) → (t : P.T x) → Hm k (P.src x t) x) {w y x : V} (t : P.T x) (u : Hm k w (P.src x t)) (v : Hm k x y) :

CategoryTheory.CategoryStruct.comp u (CategoryTheory.CategoryStruct.comp (ρ x t) v) ∈ ctxSpan P ρ w y

theorem MultiplicativeBasisDeformations.FlatPert.ctxSpan_comp {k : Type u} [CommRing k] {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (P : Pres k V) {ρ : (x : V) → (t : P.T x) → Hm k (P.src x t) x} {w y z : V} {g : Hm k w y} (hg : g ∈ ctxSpan P ρ w y) (h : Hm k y z) :

CategoryTheory.CategoryStruct.comp g h ∈ ctxSpan P ρ w z

theorem MultiplicativeBasisDeformations.FlatPert.comp_ctxSpan {k : Type u} [CommRing k] {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (P : Pres k V) {ρ : (x : V) → (t : P.T x) → Hm k (P.src x t) x} {v w y : V} {g : Hm k w y} (hg : g ∈ ctxSpan P ρ w y) (h : Hm k v w) :

CategoryTheory.CategoryStruct.comp h g ∈ ctxSpan P ρ v y

theorem MultiplicativeBasisDeformations.FlatPert.ctxSpan_le_geSpan {k : Type u} [CommRing k] {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (P : Pres k V) {ρ : (x : V) → (t : P.T x) → Hm k (P.src x t) x} {d : ℕ} (hρ : ∀ (x : V) (t : P.T x), ρ x t ∈ geSpan k d (P.src x t) x) (w y : V) :

ctxSpan P ρ w y ≤ geSpan k d w y

Ideal families and the presentation complexes #

structure MultiplicativeBasisDeformations.FlatPert.IdealFam (k : Type u) [CommRing k] (V : Type) [Quiver V] :

A two-sided ideal of kQ inside the arrow ideal.

I (w y : V) : Submodule k (Hm k w y)
comp_right {w y z : V} {g : Hm k w y} : g ∈ self.I w y → ∀ (h : Hm k y z), CategoryTheory.CategoryStruct.comp g h ∈ self.I w z
comp_left {v w y : V} {g : Hm k w y} : g ∈ self.I w y → ∀ (h : Hm k v w), CategoryTheory.CategoryStruct.comp h g ∈ self.I v y
le_ge1 (w y : V) : self.I w y ≤ geSpan k 1 w y

Instances For

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.FlatPert.Q {k : Type u} [CommRing k] {V : Type} [Quiver V] (J : IdealFam k V) (w y : V) :

The quotient kQ(w, y)/I.

Instances For

noncomputable def MultiplicativeBasisDeformations.FlatPert.compQ {k : Type u} [CommRing k] {V : Type} [Quiver V] (J : IdealFam k V) {w y z : V} (h : Hm k y z) :

Q J w y →ₗ[k] Q J w z

Right composition with a morphism on the quotients.

Instances For

theorem MultiplicativeBasisDeformations.FlatPert.compQ_mk {k : Type u} [CommRing k] {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (J : IdealFam k V) {w y z : V} (h : Hm k y z) (g : Hm k w y) :

(compQ J h) (Submodule.Quotient.mk g) = Submodule.Quotient.mk (CategoryTheory.CategoryStruct.comp g h)

noncomputable def MultiplicativeBasisDeformations.FlatPert.alpha {k : Type u} [CommRing k] {V : Type} [Quiver V] (J : IdealFam k V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] (w x : V) :

((a : (y : V) × (y ⟶ x)) → Q J w a.fst) →ₗ[k] Q J w x

The arrow map ⊕_a C(w, y_a) → C(w, x), (z_a) ↦ Σ z_a a.

Instances For

noncomputable def MultiplicativeBasisDeformations.FlatPert.relMap {k : Type u} [CommRing k] {V : Type} [Quiver V] (P : Pres k V) (J : IdealFam k V) (ρ : (x : V) → (t : P.T x) → Hm k (P.src x t) x) (w x : V) :

((t : P.T x) → Q J w (P.src x t)) →ₗ[k] (a : (y : V) × (y ⟶ x)) → Q J w a.fst

The relation map ⊕_t C(w, s_t) → ⊕_a C(w, y_a), splitting each relation by its last arrows.

Instances For

noncomputable def MultiplicativeBasisDeformations.FlatPert.epsQ {k : Type u} [CommRing k] {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (J : IdealFam k V) (x : V) :

Q J x x →ₗ[k] k

The nil coefficient on the quotient.

Instances For

theorem MultiplicativeBasisDeformations.FlatPert.proj_zero_of_ne {k : Type u} [CommRing k] {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [(x : V) → Fintype ((y : V) × (y ⟶ x))] {w x : V} (h : w ≠ x) (g : Hm k w x) :

(LinearPaths.proj 0 w x) g = 0

theorem MultiplicativeBasisDeformations.FlatPert.mem_range_alpha {k : Type u} [CommRing 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 x : V} (g : Hm k w x) (hg : (LinearPaths.proj 0 w x) g = 0) :

Submodule.Quotient.mk g ∈ (alpha J w x).range

theorem MultiplicativeBasisDeformations.FlatPert.proj_zero_endo {k : Type u} [CommRing k] {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (x : V) (g : Hm k x x) :

(LinearPaths.proj 0 x x) g = (nilCoeff x) g • CategoryTheory.CategoryStruct.id (LinearPaths.obj x)

theorem MultiplicativeBasisDeformations.FlatPert.arrow_mem_ge1 {k : Type u} [CommRing k] {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [(x : V) → Fintype ((y : V) × (y ⟶ x))] {y x : V} (b : y ⟶ x) :

LinearPaths.arrow b ∈ geSpan k 1 y x

theorem MultiplicativeBasisDeformations.FlatPert.alpha_relMap {k : Type u} [CommRing k] {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (P : Pres k V) (J : IdealFam k V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] (ρ : (x : V) → (t : P.T x) → Hm k (P.src x t) x) (hρI : ∀ (x : V) (t : P.T x) (w : V) (u : Hm k w (P.src x t)), CategoryTheory.CategoryStruct.comp u (ρ x t) ∈ J.I w x) (hρ0 : ∀ (x : V) (t : P.T x), (LinearPaths.proj 0 (P.src x t) x) (ρ x t) = 0) (w x : V) (z : (t : P.T x) → Q J w (P.src x t)) :

(alpha J w x) ((relMap P J ρ w x) z) = 0

The presentation is a complex: α ∘ ρ = 0 for relations in the ideal.

The ideals of `C` and of the perturbation `B` #

theorem MultiplicativeBasisDeformations.FlatPert.proj_eq_zero_of_geSpan {k : Type u} [CommRing k] {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [(x : V) → Fintype ((y : V) × (y ⟶ x))] {d e : ℕ} (he : e < d) {x y : V} {g : Hm k x y} (hg : g ∈ geSpan k d x y) :

(LinearPaths.proj e x y) g = 0

theorem MultiplicativeBasisDeformations.FlatPert.r_mem_ge2 {k : Type u} [CommRing k] {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (P : Pres k V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] (x : V) (t : P.T x) :

P.r x t ∈ geSpan k 2 (P.src x t) x

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

The ideal of C.

Instances For

theorem MultiplicativeBasisDeformations.FlatPert.rf_mem_ge2 {k : Type u} [CommRing 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) (x : V) (t : P.T x) :

P.r x t - f x t ∈ geSpan k 2 (P.src x t) x

noncomputable def MultiplicativeBasisDeformations.FlatPert.rf {k : Type u} [CommRing k] {V : Type} [Quiver V] (P : Pres k V) (f : (x : V) → (t : P.T x) → Hm k (P.src x t) x) (x : V) (t : P.T x) :

Hm k (P.src x t) x

The perturbed relations r_t − f_t.

Instances For

noncomputable def MultiplicativeBasisDeformations.FlatPert.idealB {k : Type u} [CommRing 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 : ℕ) :

The ideal of the perturbation B = kQ/(𝔪^{N+1}, r_t − f_t).

Instances For

Finite dimensionality #

theorem MultiplicativeBasisDeformations.FlatPert.finite_paths_eq {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)] (w : V) (n : ℕ) (y : V) :

{p : Quiver.Path w y | p.length = n}.Finite

theorem MultiplicativeBasisDeformations.FlatPert.finite_paths_lt {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)] (w y : V) (M : ℕ) :

{p : Quiver.Path w y | p.length < M}.Finite

theorem MultiplicativeBasisDeformations.FlatPert.finiteDimensional_Q {k : Type u} [CommRing k] {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (J : IdealFam k V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] [Fintype V] [(x y : V) → Fintype (x ⟶ y)] {M : ℕ} (hM : ∀ (w y : V), geSpan k M w y ≤ J.I w y) (w y : V) :

Module.Finite k (Q J w y)

A quotient killing all long paths is finite-dimensional.

Homogeneous contextual relations #

noncomputable def MultiplicativeBasisDeformations.FlatPert.hctx {k : Type u} [CommRing k] {V : Type} [Quiver V] (P : Pres k V) (d : ℕ) (w y : V) :

Submodule k (Hm k w y)

The span of the contextual relations of degree d.

Instances For

theorem MultiplicativeBasisDeformations.FlatPert.proj_ctx {k : Type u} [CommRing 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 ∈ hctx P d w y

theorem MultiplicativeBasisDeformations.FlatPert.hctx_le_B {k : Type u} [CommRing 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 ≤ d) (w y : V) :

hctx P d w y ≤ (idealB P f hf N).I w y

theorem MultiplicativeBasisDeformations.FlatPert.path_mem_B {k : Type u} [CommRing 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} (p : Quiver.Path w y) (hp : N ≤ p.length) :

LinearPaths.path p ∈ (idealB P f hf N).I w y

𝔪^N B = 0 (deformation-refinements.tex).

Exactness of the perturbed presentation at the arrow term #

theorem MultiplicativeBasisDeformations.FlatPert.rf_proj0 {k : Type u} [CommRing 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) [Fintype V] [(x y : V) → Fintype (x ⟶ y)] (x : V) (t : P.T x) (hf : ∀ (x : V) (t : P.T x), f x t ∈ geSpan k (P.deg x t + 1) (P.src x t) x) :

(LinearPaths.proj 0 (P.src x t) x) (rf P f x t) = 0

theorem MultiplicativeBasisDeformations.FlatPert.lastComp_B {k : Type u} [CommRing 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} {g : Hm k w x} (hg : g ∈ (idealB P f hf N).I w x) :

∃ (u : (t : P.T x) → Hm k w (P.src x t)), ∀ (a : (y : V) × (y ⟶ x)), (lastComp a) g - ∑ t : P.T x, CategoryTheory.CategoryStruct.comp (u t) ((lastComp a) (rf P f x t)) ∈ (idealB P f hf N).I w a.fst

Sorting contextual relations by their last factor (deformation-refinements.tex): the last-arrow components of an element of the ideal of B are, modulo the ideal, the components of a combination of the perturbed relations ending at x.

theorem MultiplicativeBasisDeformations.FlatPert.ker_alpha_B {k : Type u} [CommRing 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) :

(alpha (idealB P f hf N) w x).ker ≤ (relMap P (idealB P f hf N) (rf P f) w x).range

Exactness of the perturbed presentation at the arrow term.

theorem MultiplicativeBasisDeformations.FlatPert.span_B {k : Type u} [CommRing 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} (S : Set (Quiver.Path w y)) (hS : Submodule.span k ((fun (p : Quiver.Path w y) => Submodule.Quotient.mk (LinearPaths.path p)) '' S) = ⊤) :

Submodule.span k ((fun (p : Quiver.Path w y) => Submodule.Quotient.mk (LinearPaths.path p)) '' S) = ⊤

Classes of paths spanning C span B (the leading-term bound H_B ≤ H).

Dimensions #

theorem MultiplicativeBasisDeformations.FlatPert.geSpan_le_C {k : Type u} [CommRing 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) (w y : V) :

geSpan k N w y ≤ (idealC P).I w y

theorem MultiplicativeBasisDeformations.FlatPert.geSpan_le_B {k : Type u} [CommRing 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) :

geSpan k (N + 1) w y ≤ (idealB P f hf N).I w y

theorem MultiplicativeBasisDeformations.FlatPert.span_paths_eq_top {k : Type u} [CommRing 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)] (J : IdealFam k V) (w y : V) :

Submodule.span k (Set.range fun (p : Quiver.Path w y) => Submodule.Quotient.mk (LinearPaths.path p)) = ⊤