Corollary 12.4: polynomial mesh flatness

deformation-refinements.tex (cor:polynomial-mesh-flatness). Replace the higher coefficients in Lemma 12.3 by elements of a polynomial ring. Every fixed path basis of C is a basis of the resulting family over the polynomial ring, and it remains a basis after arbitrary base change.

The proof is the source's: spanning holds over any coefficient ring (reduction by the original relations); independence holds over the fraction field by Lemma 12.3, hence over the polynomial ring; and the free presentation is stable under base change. We prove independence over any integral domain K receiving k, and base change along any ring map K → R.

Coefficients are changed by cmap φ, which applies a ring map to every coefficient of a morphism of the path category.

Changing coefficients

noncomputable def MultiplicativeBasisDeformations.FlatPert.cmap {V : Type} [Quiver V] {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (φ : A →+* B) {x y : V} (g : Hm A x y) : Hm B x y

Coefficientwise application of a ring map AQ → BQ.

theorem MultiplicativeBasisDeformations.FlatPert.cmap_zero {V : Type} [Quiver V] {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (φ : A →+* B) {x y : V} : cmap φ 0 = 0

theorem MultiplicativeBasisDeformations.FlatPert.cmap_add {V : Type} [Quiver V] {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (φ : A →+* B) {x y : V} (g h : Hm A x y) : cmap φ (g + h) = cmap φ g + cmap φ h

theorem MultiplicativeBasisDeformations.FlatPert.cmap_smul {V : Type} [Quiver V] {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (φ : A →+* B) {x y : V} (c : A) (g : Hm A x y) : cmap φ (c • g) = φ c • cmap φ g

theorem MultiplicativeBasisDeformations.FlatPert.cmap_path {V : Type} [Quiver V] {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (φ : A →+* B) {x y : V} (p : Quiver.Path x y) : cmap φ (LinearPaths.path p) = LinearPaths.path p

noncomputable def MultiplicativeBasisDeformations.FlatPert.cmapHom {V : Type} [Quiver V] {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (φ : A →+* B) (x y : V) : Hm A x y →+ Hm B x y

cmap φ as an additive map.

theorem MultiplicativeBasisDeformations.FlatPert.cmap_sub {V : Type} [Quiver V] {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (φ : A →+* B) {x y : V} (g h : Hm A x y) : cmap φ (g - h) = cmap φ g - cmap φ h

theorem MultiplicativeBasisDeformations.FlatPert.cmap_sum {V : Type} [Quiver V] {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (φ : A →+* B) {x y : V} {ι : Type u_3} (s : Finset ι) (g : ι → Hm A x y) : cmap φ (∑ i ∈ s, g i) = ∑ i ∈ s, cmap φ (g i)

theorem MultiplicativeBasisDeformations.FlatPert.cmap_comp {V : Type} [Quiver V] {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (φ : A →+* B) {x y z : V} (g : Hm A x y) (h : Hm A y z) : cmap φ (CategoryTheory.CategoryStruct.comp g h) = CategoryTheory.CategoryStruct.comp (cmap φ g) (cmap φ h)

theorem MultiplicativeBasisDeformations.FlatPert.cmap_mem_of_span {V : Type} [Quiver V] {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (φ : A →+* B) {x y : V} {s : Set (Hm A x y)} {t : Submodule B (Hm B x y)} (h : ∀ g ∈ s, cmap φ g ∈ t) {g : Hm A x y} (hg : g ∈ Submodule.span A s) : cmap φ g ∈ t

theorem MultiplicativeBasisDeformations.FlatPert.cmap_degreePart {V : Type} [Quiver V] {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (φ : A →+* B) {d : ℕ} {x y : V} {g : Hm A x y} (hg : g ∈ LinearPaths.degreePart d x y) : cmap φ g ∈ LinearPaths.degreePart d x y

theorem MultiplicativeBasisDeformations.FlatPert.cmap_geSpan {V : Type} [Quiver V] {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (φ : A →+* B) {d : ℕ} {x y : V} {g : Hm A x y} (hg : g ∈ geSpan A d x y) : cmap φ g ∈ geSpan B d x y

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.FlatPert.Pres.map {V : Type} [Quiver V] {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (φ : A →+* B) (P : Pres A V) : Pres B V

The presentation with changed coefficients.

theorem MultiplicativeBasisDeformations.FlatPert.cmap_ctxSpan {V : Type} [Quiver V] {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (φ : A →+* B) (P : Pres A V) (ρ : (x : V) → (t : P.T x) → Hm A (P.src x t) x) {w y : V} {g : Hm A w y} (hg : g ∈ ctxSpan P ρ w y) : cmap φ g ∈ ctxSpan (Pres.map φ P) (fun (x : V) (t : (Pres.map φ P).T x) => cmap φ (ρ x t)) w y

theorem MultiplicativeBasisDeformations.FlatPert.cmap_idealC {V : Type} [Quiver V] {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (φ : A →+* B) (P : Pres A V) [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [(x : V) → Fintype ((y : V) × (y ⟶ x))] {w y : V} {g : Hm A w y} (hg : g ∈ (idealC P).I w y) : cmap φ g ∈ (idealC (Pres.map φ P)).I w y

noncomputable def MultiplicativeBasisDeformations.FlatPert.fmap {V : Type} [Quiver V] {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (φ : A →+* B) (P : Pres A V) (f : (x : V) → (t : P.T x) → Hm A (P.src x t) x) (x : V) (t : (Pres.map φ P).T x) : Hm B ((Pres.map φ P).src x t) x

The perturbation with changed coefficients.

theorem MultiplicativeBasisDeformations.FlatPert.hf_map {V : Type} [Quiver V] {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (φ : A →+* B) (P : Pres A V) [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (f : (x : V) → (t : P.T x) → Hm A (P.src x t) x) (hf : ∀ (x : V) (t : P.T x), f x t ∈ geSpan A (P.deg x t + 1) (P.src x t) x) (x : V) (t : (Pres.map φ P).T x) : fmap φ P f x t ∈ geSpan B ((Pres.map φ P).deg x t + 1) ((Pres.map φ P).src x t) x

theorem MultiplicativeBasisDeformations.FlatPert.rf_map {V : Type} [Quiver V] {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (φ : A →+* B) (P : Pres A V) [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (f : (x : V) → (t : P.T x) → Hm A (P.src x t) x) (x : V) (t : P.T x) : rf (Pres.map φ P) (fmap φ P f) x t = cmap φ (rf P f x t)

theorem MultiplicativeBasisDeformations.FlatPert.cmap_idealB {V : Type} [Quiver V] {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (φ : A →+* B) (P : Pres A V) [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (f : (x : V) → (t : P.T x) → Hm A (P.src x t) x) (hf : ∀ (x : V) (t : P.T x), f x t ∈ geSpan A (P.deg x t + 1) (P.src x t) x) (N : ℕ) {w y : V} {g : Hm A w y} (hg : g ∈ (idealB P f hf N).I w y) : cmap φ g ∈ (idealB (Pres.map φ P) (fmap φ P f) ⋯ N).I w y

theorem MultiplicativeBasisDeformations.FlatPert.hN_map {V : Type} [Quiver V] {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (φ : A →+* B) (P : Pres A V) [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (N : ℕ) (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) : N ≤ p.length → LinearPaths.path p ∈ ctxSpan (Pres.map φ P) (Pres.map φ P).r w y

Spanning and independence of path classes

theorem MultiplicativeBasisDeformations.FlatPert.span_classes_eq_top_iff {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [(x : V) → Fintype ((y : V) × (y ⟶ x))] {A : Type u_1} [CommRing A] (J : IdealFam A V) {w y : V} {ι : Type u_2} (p : ι → Quiver.Path w y) : Submodule.span A (Set.range fun (i : ι) => Submodule.Quotient.mk (LinearPaths.path (p i))) = ⊤ ↔ ∀ (q : Quiver.Path w y), LinearPaths.path q ∈ Submodule.span A (Set.range fun (i : ι) => LinearPaths.path (p i)) ⊔ J.I w y

Spanning criterion: path classes span AQ/J iff every path is a combination of them modulo J.

theorem MultiplicativeBasisDeformations.FlatPert.span_classes_map {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [(x : V) → Fintype ((y : V) × (y ⟶ x))] {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (φ : A →+* B) (JA : IdealFam A V) (JB : IdealFam B V) (hJ : ∀ (w y : V), ∀ g ∈ JA.I w y, cmap φ g ∈ JB.I w y) {w y : V} {ι : Type u_3} (p : ι → Quiver.Path w y) (h : Submodule.span A (Set.range fun (i : ι) => Submodule.Quotient.mk (LinearPaths.path (p i))) = ⊤) : Submodule.span B (Set.range fun (i : ι) => Submodule.Quotient.mk (LinearPaths.path (p i))) = ⊤

Spanning passes along coefficient changes.

theorem MultiplicativeBasisDeformations.FlatPert.linInd_classes_comap {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [(x : V) → Fintype ((y : V) × (y ⟶ x))] {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (φ : A →+* B) (hφ : Function.Injective ⇑φ) (JA : IdealFam A V) (JB : IdealFam B V) (hJ : ∀ (w y : V), ∀ g ∈ JA.I w y, cmap φ g ∈ JB.I w y) {w y : V} {ι : Type u_3} [Fintype ι] (p : ι → Quiver.Path w y) (h : LinearIndependent B fun (i : ι) => Submodule.Quotient.mk (LinearPaths.path (p i))) : LinearIndependent A fun (i : ι) => Submodule.Quotient.mk (LinearPaths.path (p i))

Independence descends along injective coefficient changes.

Over a fraction field: Lemma 12.3 with extended coefficients

theorem MultiplicativeBasisDeformations.FlatPert.finrank_le_of_span {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)] {k : Type u} {F : Type u_1} [Field k] [Field F] (JA : IdealFam k V) (JB : IdealFam F V) (w y : V) [FiniteDimensional k (Q JA w y)] (hspan : ∀ {ι : Type u} (p : ι → Quiver.Path w y), Submodule.span k (Set.range fun (i : ι) => Submodule.Quotient.mk (LinearPaths.path (p i))) = ⊤ → Submodule.span F (Set.range fun (i : ι) => Submodule.Quotient.mk (LinearPaths.path (p i))) = ⊤) : Module.finrank F (Q JB w y) ≤ Module.finrank k (Q JA w y)

If path classes spanning Q JA always span Q JB, then dim Q JB ≤ dim Q JA.

theorem MultiplicativeBasisDeformations.FlatPert.span_B_of_C {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)] {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (φ : A →+* B) (P : Pres A V) (N : ℕ) (hN : ∀ (w y : V) (p : Quiver.Path w y), N ≤ p.length → LinearPaths.path p ∈ ctxSpan P P.r w y) (f : (x : V) → (t : (Pres.map φ P).T x) → Hm B ((Pres.map φ P).src x t) x) (hf : ∀ (x : V) (t : (Pres.map φ P).T x), f x t ∈ geSpan B ((Pres.map φ P).deg x t + 1) ((Pres.map φ P).src x t) x) {w y : V} {ι : Type u_3} (p : ι → Quiver.Path w y) (h : Submodule.span A (Set.range fun (i : ι) => Submodule.Quotient.mk (LinearPaths.path (p i))) = ⊤) : Submodule.span B (Set.range fun (i : ι) => Submodule.Quotient.mk (LinearPaths.path (p i))) = ⊤

Spanning of the perturbation from spanning of C, after a change of coefficients.

theorem MultiplicativeBasisDeformations.FlatPert.finrank_B_field {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)] {k : Type u} {K : Type u_1} {F : Type u_2} [Field k] [CommRing K] [Field F] (ι₀ : k →+* K) (j : K →+* F) (P : Pres k V) (N : ℕ) (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) (f : (x : V) → (t : (Pres.map ι₀ P).T x) → Hm K ((Pres.map ι₀ P).src x t) x) (hf : ∀ (x : V) (t : (Pres.map ι₀ P).T x), f x t ∈ geSpan K ((Pres.map ι₀ P).deg x t + 1) ((Pres.map ι₀ P).src x t) x) (w y : V) : Module.finrank F (Q (idealB (Pres.map j (Pres.map ι₀ P)) (fmap j (Pres.map ι₀ P) f) ⋯ N) w y) = Module.finrank k (Q (idealC P) w y)

Lemma 12.3 after extending coefficients to a field: the perturbation over F has the dimensions of C over k.

theorem MultiplicativeBasisDeformations.FlatPert.path_basis_domain {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)] {k : Type u} {K : Type u_1} [Field k] [CommRing K] (ι₀ : k →+* K) (P : Pres k V) (N : ℕ) (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) (f : (x : V) → (t : (Pres.map ι₀ P).T x) → Hm K ((Pres.map ι₀ P).src x t) x) (hf : ∀ (x : V) (t : (Pres.map ι₀ P).T x), f x t ∈ geSpan K ((Pres.map ι₀ P).deg x t + 1) ((Pres.map ι₀ P).src x t) x) [IsDomain K] {w y : V} {ι : Type u_3} [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))) = ⊤

Independence over an integral domain (cor:polynomial-mesh-flatness, first part): a path basis of C is a basis of the perturbation with coefficients in any domain K ⊇ k.

Base change

theorem MultiplicativeBasisDeformations.FlatPert.path_basis_baseChange {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [(x : V) → Fintype ((y : V) × (y ⟶ x))] {K : Type u_1} {R : Type u_2} [CommRing K] [CommRing R] (φ : K →+* R) (P : Pres K V) (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 : ℕ) {w y : V} {ι : Type u_3} [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 R fun (i : ι) => Submodule.Quotient.mk (LinearPaths.path (p i))) ∧ Submodule.span R (Set.range fun (i : ι) => Submodule.Quotient.mk (LinearPaths.path (p i))) = ⊤

Base change of a free presentation (cor:polynomial-mesh-flatness, second part): if the classes of a path family are a basis of the perturbation over K, they are a basis of the perturbation over R with coefficients changed along φ : K → R.

Corollary 12.4

theorem MultiplicativeBasisDeformations.FlatPert.polynomial_flatness {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)] {k : Type u} [Field k] (P : Pres k V) (N : ℕ) (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) {σ : Type u_1} (f : (x : V) → (t : (Pres.map MvPolynomial.C P).T x) → Hm (MvPolynomial σ k) ((Pres.map MvPolynomial.C P).src x t) x) (hf : ∀ (x : V) (t : (Pres.map MvPolynomial.C P).T x), f x t ∈ geSpan (MvPolynomial σ k) ((Pres.map MvPolynomial.C P).deg x t + 1) ((Pres.map MvPolynomial.C P).src x t) x) {w y : V} {ι : Type u_2} [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 (MvPolynomial σ k) fun (i : ι) => Submodule.Quotient.mk (LinearPaths.path (p i))) ∧ Submodule.span (MvPolynomial σ k) (Set.range fun (i : ι) => Submodule.Quotient.mk (LinearPaths.path (p i))) = ⊤) ∧ ∀ {R : Type u_3} [inst : CommRing R] (φ : MvPolynomial σ k →+* R), (LinearIndependent R fun (i : ι) => Submodule.Quotient.mk (LinearPaths.path (p i))) ∧ Submodule.span R (Set.range fun (i : ι) => Submodule.Quotient.mk (LinearPaths.path (p i))) = ⊤

Corollary 12.4 (cor:polynomial-mesh-flatness): in the setting of Lemma 12.3, take the higher terms f with coefficients in a polynomial ring K = k[t_σ]. Every path basis of C is a basis of the family B_K = KQ/(𝔪^{N+1}, r − f) over K, and remains a basis after base change along any ring map K → R.