Twisting weight-homogeneous data by parameters (toward Proposition 12.8)

deformation-refinements.tex: "Give t_i total weight −χ_i, or equivalently coefficient weight χ_i. The choices above, made separately in each weight, make F_j homogeneous". Conversely, data at t = 1 whose components have relative weights in the monoid C of the χ_i define polynomial families: the component of relative weight γ is multiplied by t^{coords γ}, where coords : Wt →+ (I → ℤ) sends χ_i to the i-th unit vector (twl for linear maps, twb for bilinear maps). For t in the torus this is conjugation by the diagonal scaling S_t (twb_torus, twl_torus), so twisting preserves all identities there; the twisted data are polynomial in t (IsPoly), so the identities hold for every t.

def MultiplicativeBasisDeformations.MGr.ch {k : Type u_1} [Field k] {Wt : Type u_2} [AddCommGroup Wt] {I : Type} [Fintype I] (coords : Wt →+ I → ℤ) (t : I → k) (γ : Wt) : k

The polynomial character t^{coords γ} (exponents truncated at 0).

def MultiplicativeBasisDeformations.MGr.chz {k : Type u_1} [Field k] {Wt : Type u_2} [AddCommGroup Wt] {I : Type} [Fintype I] (coords : Wt →+ I → ℤ) (t : I → k) (γ : Wt) : k

The torus character t^{coords γ} with integer exponents.

theorem MultiplicativeBasisDeformations.MGr.chz_add {k : Type u_1} [Field k] {Wt : Type u_2} [AddCommGroup Wt] [DecidableEq Wt] {I : Type} [Fintype I] [DecidableEq I] {coords : Wt →+ I → ℤ} {t : I → k} (ht : ∀ (i : I), t i ≠ 0) (γ δ : Wt) : chz coords t (γ + δ) = chz coords t γ * chz coords t δ

theorem MultiplicativeBasisDeformations.MGr.chz_zero {k : Type u_1} [Field k] {Wt : Type u_2} [AddCommGroup Wt] [DecidableEq Wt] {I : Type} [Fintype I] [DecidableEq I] {coords : Wt →+ I → ℤ} (t : I → k) : chz coords t 0 = 1

theorem MultiplicativeBasisDeformations.MGr.chz_ne_zero {k : Type u_1} [Field k] {Wt : Type u_2} [AddCommGroup Wt] [DecidableEq Wt] {I : Type} [Fintype I] [DecidableEq I] {coords : Wt →+ I → ℤ} {t : I → k} (ht : ∀ (i : I), t i ≠ 0) (γ : Wt) : chz coords t γ ≠ 0

theorem MultiplicativeBasisDeformations.MGr.chz_neg {k : Type u_1} [Field k] {Wt : Type u_2} [AddCommGroup Wt] [DecidableEq Wt] {I : Type} [Fintype I] [DecidableEq I] {coords : Wt →+ I → ℤ} {t : I → k} (ht : ∀ (i : I), t i ≠ 0) (γ : Wt) : chz coords t (-γ) = (chz coords t γ)⁻¹

theorem MultiplicativeBasisDeformations.MGr.chz_sub {k : Type u_1} [Field k] {Wt : Type u_2} [AddCommGroup Wt] [DecidableEq Wt] {I : Type} [Fintype I] [DecidableEq I] {coords : Wt →+ I → ℤ} {t : I → k} (ht : ∀ (i : I), t i ≠ 0) (γ δ : Wt) : chz coords t (γ - δ) = chz coords t γ * (chz coords t δ)⁻¹

theorem MultiplicativeBasisDeformations.MGr.ch_eq_chz {k : Type u_1} [Field k] {Wt : Type u_2} [AddCommGroup Wt] [DecidableEq Wt] {I : Type} [Fintype I] [DecidableEq I] {coords : Wt →+ I → ℤ} {t : I → k} {γ : Wt} (hγ : ∀ (i : I), 0 ≤ coords γ i) : ch coords t γ = chz coords t γ

theorem MultiplicativeBasisDeformations.MGr.ch_one {k : Type u_1} [Field k] {Wt : Type u_2} [AddCommGroup Wt] [DecidableEq Wt] {I : Type} [Fintype I] [DecidableEq I] {coords : Wt →+ I → ℤ} (γ : Wt) : ch coords (fun (x : I) => 1) γ = 1

theorem MultiplicativeBasisDeformations.MGr.coords_nonneg_of_le {Wt : Type u_2} [AddCommGroup Wt] [DecidableEq Wt] {I : Type} [Fintype I] [DecidableEq I] {coords : Wt →+ I → ℤ} {C : AddSubmonoid Wt} (hC : ∀ γ ∈ C, ∀ (i : I), 0 ≤ coords γ i) {γ : Wt} (hγ : γ ∈ C) (i : I) : 0 ≤ coords γ i

The weights of the cone have nonnegative coordinates when the generators do.

def MultiplicativeBasisDeformations.MGr.scale {k : Type u_1} [Field k] {Wt : Type u_2} [AddCommGroup Wt] [DecidableEq Wt] {I : Type} [Fintype I] (coords : Wt →+ I → ℤ) {N : Type u_3} [AddCommGroup N] [Module k N] (G : MGr k Wt N) (t : I → k) : N →ₗ[k] N

The diagonal scaling m ↦ t^{coords β} m on weight β.

theorem MultiplicativeBasisDeformations.MGr.scale_hom {k : Type u_1} [Field k] {Wt : Type u_2} [AddCommGroup Wt] [DecidableEq Wt] {I : Type} [Fintype I] [DecidableEq I] {coords : Wt →+ I → ℤ} {N : Type u_3} [AddCommGroup N] [Module k N] (G : MGr k Wt N) (t : I → k) {β : Wt} {n : N} (hn : G.IsHom β n) : (scale coords G t) n = chz coords t β • n

theorem MultiplicativeBasisDeformations.MGr.chz_inv {k : Type u_1} [Field k] {Wt : Type u_2} [AddCommGroup Wt] [DecidableEq Wt] {I : Type} [Fintype I] [DecidableEq I] {coords : Wt →+ I → ℤ} (t : I → k) (β : Wt) : chz coords (fun (i : I) => (t i)⁻¹) β = (chz coords t β)⁻¹

theorem MultiplicativeBasisDeformations.MGr.scale_inv_scale {k : Type u_1} [Field k] {Wt : Type u_2} [AddCommGroup Wt] [DecidableEq Wt] {I : Type} [Fintype I] [DecidableEq I] {coords : Wt →+ I → ℤ} {N : Type u_3} [AddCommGroup N] [Module k N] (G : MGr k Wt N) {t : I → k} (ht : ∀ (i : I), t i ≠ 0) (n : N) : (scale coords G fun (i : I) => (t i)⁻¹) ((scale coords G t) n) = n

theorem MultiplicativeBasisDeformations.MGr.scale_scale_inv {k : Type u_1} [Field k] {Wt : Type u_2} [AddCommGroup Wt] [DecidableEq Wt] {I : Type} [Fintype I] [DecidableEq I] {coords : Wt →+ I → ℤ} {N : Type u_3} [AddCommGroup N] [Module k N] (G : MGr k Wt N) {t : I → k} (ht : ∀ (i : I), t i ≠ 0) (n : N) : (scale coords G t) ((scale coords G fun (i : I) => (t i)⁻¹) n) = n

Twisting linear and bilinear maps

def MultiplicativeBasisDeformations.MGr.twl {k : Type u_1} [Field k] {Wt : Type u_2} [AddCommGroup Wt] [DecidableEq Wt] {I : Type} [Fintype I] (coords : Wt →+ I → ℤ) {N : Type u_3} {N' : Type u_4} [AddCommGroup N] [Module k N] [AddCommGroup N'] [Module k N'] (G : MGr k Wt N) (G' : MGr k Wt N') (t : I → k) (ρ : Wt) (f : N →ₗ[k] N') : N →ₗ[k] N'

The twist of a linear map relative to the weight ρ.

def MultiplicativeBasisDeformations.MGr.twb {k : Type u_1} [Field k] {Wt : Type u_2} [AddCommGroup Wt] [DecidableEq Wt] {I : Type} [Fintype I] (coords : Wt →+ I → ℤ) {N : Type u_3} {N' : Type u_4} {N'' : Type u_5} [AddCommGroup N] [Module k N] [AddCommGroup N'] [Module k N'] [AddCommGroup N''] [Module k N''] (G : MGr k Wt N) (G' : MGr k Wt N') (G'' : MGr k Wt N'') (t : I → k) (ρ : Wt) (φ : N →ₗ[k] N' →ₗ[k] N'') : N →ₗ[k] N' →ₗ[k] N''

The twist of a bilinear map relative to the weight ρ.

theorem MultiplicativeBasisDeformations.MGr.twl_hom {k : Type u_1} [Field k] {Wt : Type u_2} [AddCommGroup Wt] [DecidableEq Wt] {I : Type} [Fintype I] [DecidableEq I] {coords : Wt →+ I → ℤ} {N : Type u_3} {N' : Type u_4} [AddCommGroup N] [Module k N] [AddCommGroup N'] [Module k N'] (G : MGr k Wt N) (G' : MGr k Wt N') (t : I → k) (ρ : Wt) (f : N →ₗ[k] N') {β : Wt} {n : N} (hn : G.IsHom β n) : (twl coords G G' t ρ f) n = ∑ δ ∈ G'.supp, ch coords t (δ - β - ρ) • (G'.proj δ) (f n)

theorem MultiplicativeBasisDeformations.MGr.twb_hom {k : Type u_1} [Field k] {Wt : Type u_2} [AddCommGroup Wt] [DecidableEq Wt] {I : Type} [Fintype I] [DecidableEq I] {coords : Wt →+ I → ℤ} {N : Type u_3} {N' : Type u_4} {N'' : Type u_5} [AddCommGroup N] [Module k N] [AddCommGroup N'] [Module k N'] [AddCommGroup N''] [Module k N''] (G : MGr k Wt N) (G' : MGr k Wt N') (G'' : MGr k Wt N'') (t : I → k) (ρ : Wt) (φ : N →ₗ[k] N' →ₗ[k] N'') {β α : Wt} {n : N} {n' : N'} (hn : G.IsHom β n) (hn' : G'.IsHom α n') : ((twb coords G G' G'' t ρ φ) n) n' = ∑ δ ∈ G''.supp, ch coords t (δ - β - α - ρ) • (G''.proj δ) ((φ n) n')

theorem MultiplicativeBasisDeformations.MGr.twb_torus {k : Type u_1} [Field k] {Wt : Type u_2} [AddCommGroup Wt] [DecidableEq Wt] {I : Type} [Fintype I] [DecidableEq I] {coords : Wt →+ I → ℤ} {C : AddSubmonoid Wt} {N : Type u_3} {N' : Type u_4} {N'' : Type u_5} [AddCommGroup N] [Module k N] [AddCommGroup N'] [Module k N'] [AddCommGroup N''] [Module k N''] {G : MGr k Wt N} {G' : MGr k Wt N'} {G'' : MGr k Wt N''} (hC : ∀ γ ∈ C, ∀ (i : I), 0 ≤ coords γ i) {t : I → k} (ht : ∀ (i : I), t i ≠ 0) {ρ : Wt} {φ : N →ₗ[k] N' →ₗ[k] N''} (hφ : ConeBil ρ φ) (n : N) (n' : N') : ((twb coords G G' G'' t ρ φ) n) n' = (chz coords t ρ)⁻¹ • (scale coords G'' t) ((φ ((scale coords G fun (i : I) => (t i)⁻¹) n)) ((scale coords G' fun (i : I) => (t i)⁻¹) n'))

On the torus, twisting a bilinear map in the cone is conjugation by the scalings.

theorem MultiplicativeBasisDeformations.MGr.twl_torus {k : Type u_1} [Field k] {Wt : Type u_2} [AddCommGroup Wt] [DecidableEq Wt] {I : Type} [Fintype I] [DecidableEq I] {coords : Wt →+ I → ℤ} {C : AddSubmonoid Wt} {N : Type u_3} {N' : Type u_4} [AddCommGroup N] [Module k N] [AddCommGroup N'] [Module k N'] {G : MGr k Wt N} {G' : MGr k Wt N'} (hC : ∀ γ ∈ C, ∀ (i : I), 0 ≤ coords γ i) {t : I → k} (ht : ∀ (i : I), t i ≠ 0) {ρ : Wt} {f : N →ₗ[k] N'} (hf : ConeLin ρ f) (n : N) : (twl coords G G' t ρ f) n = (chz coords t ρ)⁻¹ • (scale coords G' t) (f ((scale coords G fun (i : I) => (t i)⁻¹) n))

On the torus, twisting a linear map in the cone is conjugation by the scalings.

Polynomiality

theorem MultiplicativeBasisDeformations.MGr.isPoly_ch {k : Type u_1} [Field k] {Wt : Type u_2} [AddCommGroup Wt] [DecidableEq Wt] {I : Type} [Fintype I] [DecidableEq I] {coords : Wt →+ I → ℤ} (γ : Wt) : IsPoly fun (t : I → k) => ch coords t γ • 1

theorem MultiplicativeBasisDeformations.MGr.isPoly_twl {k : Type u_1} [Field k] {Wt : Type u_2} [AddCommGroup Wt] [DecidableEq Wt] {I : Type} [Fintype I] [DecidableEq I] {coords : Wt →+ I → ℤ} {N : Type u_3} {N' : Type u_4} [AddCommGroup N] [Module k N] [AddCommGroup N'] [Module k N'] (G : MGr k Wt N) (G' : MGr k Wt N') (ρ : Wt) (f : N →ₗ[k] N') : IsPoly fun (t : I → k) => twl coords G G' t ρ f

theorem MultiplicativeBasisDeformations.MGr.isPoly_twb {k : Type u_1} [Field k] {Wt : Type u_2} [AddCommGroup Wt] [DecidableEq Wt] {I : Type} [Fintype I] [DecidableEq I] {coords : Wt →+ I → ℤ} {N : Type u_3} {N' : Type u_4} {N'' : Type u_5} [AddCommGroup N] [Module k N] [AddCommGroup N'] [Module k N'] [AddCommGroup N''] [Module k N''] (G : MGr k Wt N) (G' : MGr k Wt N') (G'' : MGr k Wt N'') (ρ : Wt) (φ : N →ₗ[k] N' →ₗ[k] N'') : IsPoly fun (t : I → k) => twb coords G G' G'' t ρ φ