Binary normalization #
Corollary 7.8 (cor:binary-normalization, characteristic-two-construction.tex):
if Λ also has a compatible grading by a lattice L, with S in degree zero,
μ_i raising L-degree by χ_i, and the χ_i part of an integer basis of
L, then every positive filtered deformation is isomorphic to a fibre with all
parameters zero or one, and two parameter vectors with the same zero coordinates
give isomorphic fibres. "For a : L → k^*, multiply a vector of weight ℓ by
a(ℓ). This is an automorphism of (Λ, m), and transporting m_λ along it
changes its coefficients to λ'_i = λ_i a(χ_i)."
The lattice grading is LatGrading (finitely supported projections, as for the
length grading); characters are additive maps L → Additive kˣ, extended from
the prescribed values on the χ_i through the basis (exists_character).
structure
MultiplicativeBasisDeformations.LatGrading
(k : Type u)
[Field k]
(Λ : Type v)
[Ring Λ]
[Algebra k Λ]
(L : Type)
[AddCommGroup L]
[DecidableEq L]
:
Type v
A grading by an abelian group L, with finitely many nonzero components.
- proj : L → Λ →ₗ[k] Λ
- supp : Finset L
Instances For
def
MultiplicativeBasisDeformations.LatGrading.IsHom
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{L : Type}
[AddCommGroup L]
[DecidableEq L]
(W : LatGrading k Λ L)
(l : L)
(x : Λ)
:
A homogeneous element of weight l.
Instances For
theorem
MultiplicativeBasisDeformations.LatGrading.isHom_proj
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{L : Type}
[AddCommGroup L]
[DecidableEq L]
(W : LatGrading k Λ L)
(l : L)
(x : Λ)
:
theorem
MultiplicativeBasisDeformations.LatGrading.isHom_mul
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{L : Type}
[AddCommGroup L]
[DecidableEq L]
(W : LatGrading k Λ L)
{l l' : L}
{x y : Λ}
(hx : W.IsHom l x)
(hy : W.IsHom l' y)
:
W.IsHom (l + l') (x * y)
theorem
MultiplicativeBasisDeformations.LatGrading.proj_of_isHom
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{L : Type}
[AddCommGroup L]
[DecidableEq L]
(W : LatGrading k Λ L)
{l l' : L}
{x : Λ}
(hx : W.IsHom l x)
:
(W.proj l') x = if l = l' then x else 0
def
MultiplicativeBasisDeformations.LatGrading.rescale
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{L : Type}
[AddCommGroup L]
[DecidableEq L]
(W : LatGrading k Λ L)
(a : L → kˣ)
:
Λ →ₗ[k] Λ
Rescaling by a character a: multiply the weight-l part by a(l).
Instances For
theorem
MultiplicativeBasisDeformations.LatGrading.rescale_hom
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{L : Type}
[AddCommGroup L]
[DecidableEq L]
(W : LatGrading k Λ L)
(a : L → kˣ)
{l : L}
{x : Λ}
(hx : W.IsHom l x)
:
(W.rescale a) x = ↑(a l) • x
theorem
MultiplicativeBasisDeformations.LatGrading.rescale_apply
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{L : Type}
[AddCommGroup L]
[DecidableEq L]
(W : LatGrading k Λ L)
(a : L → kˣ)
(x : Λ)
:
theorem
MultiplicativeBasisDeformations.LatGrading.rescale_mul
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{L : Type}
[AddCommGroup L]
[DecidableEq L]
{W : LatGrading k Λ L}
{a : L → kˣ}
(ha : ∀ (l l' : L), a (l + l') = a l * a l')
(x y : Λ)
:
theorem
MultiplicativeBasisDeformations.LatGrading.rescale_of_raises
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{L : Type}
[AddCommGroup L]
[DecidableEq L]
{W : LatGrading k Λ L}
{a : L → kˣ}
(ha : ∀ (l l' : L), a (l + l') = a l * a l')
{χ : L}
{μ : Λ →ₗ[k] Λ →ₗ[k] Λ}
(hμ : ∀ (l l' : L) (x y : Λ), W.IsHom l x → W.IsHom l' y → W.IsHom (l + l' + χ) ((μ x) y))
(x y : Λ)
:
theorem
MultiplicativeBasisDeformations.LatGrading.rescale_comp
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{L : Type}
[AddCommGroup L]
[DecidableEq L]
{W : LatGrading k Λ L}
{a b : L → kˣ}
(x : Λ)
:
theorem
MultiplicativeBasisDeformations.LatGrading.rescale_one
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{L : Type}
[AddCommGroup L]
[DecidableEq L]
{W : LatGrading k Λ L}
(x : Λ)
:
(W.rescale fun (x : L) => 1) x = x
def
MultiplicativeBasisDeformations.LatGrading.rescaleEquiv
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{L : Type}
[AddCommGroup L]
[DecidableEq L]
{W : LatGrading k Λ L}
(a : L → kˣ)
:
Λ ≃ₗ[k] Λ
The rescaling as a linear automorphism.
Instances For
theorem
MultiplicativeBasisDeformations.LatGrading.rescaleEquiv_apply
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{L : Type}
[AddCommGroup L]
[DecidableEq L]
{W : LatGrading k Λ L}
(a : L → kˣ)
(x : Λ)
:
(rescaleEquiv a) x = (W.rescale a) x
theorem
MultiplicativeBasisDeformations.LatGrading.rescaleEquiv_symm_apply
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{L : Type}
[AddCommGroup L]
[DecidableEq L]
{W : LatGrading k Λ L}
(a : L → kˣ)
(x : Λ)
:
(rescaleEquiv a).symm x = (W.rescale fun (l : L) => (a l)⁻¹) x
theorem
MultiplicativeBasisDeformations.exists_character
{k : Type u}
[Field k]
{L : Type}
[AddCommGroup L]
[DecidableEq L]
{ι : Type}
(b : Module.Basis ι ℤ L)
{n : ℕ}
(j : Fin n → ι)
(hj : Function.Injective j)
(w : Fin n → kˣ)
:
∃ (a : L → kˣ), (∀ (l l' : L), a (l + l') = a l * a l') ∧ a 0 = 1 ∧ ∀ (i : Fin n), a (b (j i)) = w i
Characters from part of a basis: prescribed values on part of an
integer basis extend to a character L → k^*.
theorem
MultiplicativeBasisDeformations.LenGrading.proj_rescale
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{L : Type}
[AddCommGroup L]
[DecidableEq L]
{W : LatGrading k Λ L}
{G : LenGrading k Λ}
(compat : ∀ (d : ℕ) (l : L) (x : Λ), (G.proj d) ((W.proj l) x) = (W.proj l) ((G.proj d) x))
(a : L → kˣ)
(d : ℕ)
(x : Λ)
:
theorem
MultiplicativeBasisDeformations.LenGrading.ge_rescale
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{L : Type}
[AddCommGroup L]
[DecidableEq L]
{W : LatGrading k Λ L}
{G : LenGrading k Λ}
(compat : ∀ (d : ℕ) (l : L) (x : Λ), (G.proj d) ((W.proj l) x) = (W.proj l) ((G.proj d) x))
(a : L → kˣ)
{d : ℕ}
{x : Λ}
(hx : G.Ge d x)
:
theorem
MultiplicativeBasisDeformations.LenGrading.rescale_mLam
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{L : Type}
[AddCommGroup L]
[DecidableEq L]
{W : LatGrading k Λ L}
{n : ℕ}
{μ : Fin n → Λ →ₗ[k] Λ →ₗ[k] Λ}
{χ : Fin n → L}
(hχ : ∀ (i : Fin n) (l l' : L) (x y : Λ), W.IsHom l x → W.IsHom l' y → W.IsHom (l + l' + χ i) (((μ i) x) y))
{a : L → kˣ}
(ha : ∀ (l l' : L), a (l + l') = a l * a l')
(lam : Fin n → k)
(x y : Λ)
:
theorem
MultiplicativeBasisDeformations.LenGrading.binaryNormalization
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{L : Type}
[AddCommGroup L]
[DecidableEq L]
{W : LatGrading k Λ L}
{G : LenGrading k Λ}
{V : G.Vertices}
(compat : ∀ (d : ℕ) (l : L) (x : Λ), (G.proj d) ((W.proj l) x) = (W.proj l) ((G.proj d) x))
{n : ℕ}
{μ : Fin n → Λ →ₗ[k] Λ →ₗ[k] Λ}
{χ : Fin n → L}
(hχ : ∀ (i : Fin n) (l l' : L) (x y : Λ), W.IsHom l x → W.IsHom l' y → W.IsHom (l + l' + χ i) (((μ i) x) y))
{qd : Fin n → ℕ}
(H : FamilyHyp V μ qd)
(he0 : ∀ (i : Fin V.n), W.IsHom 0 (V.e i))
(hbasis : ∃ (ι : Type) (b : Module.Basis ι ℤ L) (j : Fin n → ι), Function.Injective j ∧ ∀ (i : Fin n), b (j i) = χ i)
{B : Type w}
[Ring B]
[Algebra k B]
(P : PosFiltration G B)
:
(∃ (lam : Fin n → k),
(∀ (i : Fin n), lam i = 0 ∨ lam i = 1) ∧ ∃ (Ψ : Λ ≃ₗ[k] B),
(∀ (a b : Λ), Ψ (((mLam μ lam) a) b) = Ψ a * Ψ b) ∧ (CompleteOrthogonalIdempotents fun (i : Fin V.n) => Ψ (V.e i)) ∧ (∀ (d : ℕ), Submodule.map (↑Ψ) (G.geSub d) = P.F d) ∧ ∃ (c : L → kˣ), ∀ (d : ℕ) (l : L) (x : Λ), G.IsHom d x → W.IsHom l x → (P.σ d) (Ψ x) = ↑(c l) • x) ∧ ∀ (lam lam' : Fin n → k),
(∀ (i : Fin n), lam i = 0 ↔ lam' i = 0) →
∃ (R : Λ ≃ₗ[k] Λ), ∀ (a b : Λ), R (((mLam μ lam) a) b) = ((mLam μ lam') (R a)) (R b)
Corollary 7.8 (binary normalization).