Local corners are truncated polynomial algebras #
Lemma 3.1(2) (projective-rays.tex): "Every subspace of rad C/(rad C)²
lifts to an ideal, so this space has dimension at most one […]. A lift t of a
generator generates successive radical powers, by Nakayama's lemma. Nilpotence
then writes every element as a polynomial in t, giving C ≅ k[t]/(t^N)."
Here the ideals of C = R_x are the endpoint subbimodules of A(x, x), which
form a chain (Lemma 3.1(3), isChain_subbimodules); this gives
rad C = k t + (rad C)² (exists_rad_gen). Nakayama's lemma for subbimodules
gives rad C ⊆ C t C, and Lemma 3.1(3) makes C t C one-sided, C t or
t C; so every element is a polynomial in t (aeval_surjective). The kernel of
k[X] → C is (X^N) with N the nilpotency index of t.
theorem
MultiplicativeBasisDeformations.PrimitiveIdempotents.cornerRadical_mul_le
{k : Type u}
[Field k]
[IsAlgClosed k]
{A : Type v}
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
(F : PrimitiveIdempotents A)
(x : Fin F.m)
:
F.cornerRadical x * F.cornerRadical x ≤ F.cornerRadical x
theorem
MultiplicativeBasisDeformations.PrimitiveIdempotents.e_mul_of_mem
{k : Type u}
[Field k]
[IsAlgClosed k]
{A : Type v}
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
(F : PrimitiveIdempotents A)
{x y : Fin F.m}
{a : A}
(ha : a ∈ F.corner x y)
:
F.e x * a = a
theorem
MultiplicativeBasisDeformations.PrimitiveIdempotents.mul_e_of_mem
{k : Type u}
[Field k]
[IsAlgClosed k]
{A : Type v}
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
(F : PrimitiveIdempotents A)
{x y : Fin F.m}
{a : A}
(ha : a ∈ F.corner x y)
:
a * F.e y = a
theorem
MultiplicativeBasisDeformations.PrimitiveIdempotents.exists_sub_smul_mem_cornerRadical
{k : Type u}
[Field k]
[IsAlgClosed k]
{A : Type v}
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
(F : PrimitiveIdempotents A)
(x : Fin F.m)
{a : A}
(ha : a ∈ F.corner x x)
:
∃ (c : k), a - c • F.e x ∈ F.cornerRadical x
a - c e_x ∈ rad R_x for some scalar c.
theorem
MultiplicativeBasisDeformations.PrimitiveIdempotents.isEndpoint_of_between
{k : Type u}
[Field k]
[IsAlgClosed k]
{A : Type v}
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
(F : PrimitiveIdempotents A)
(x : Fin F.m)
{V : Submodule k A}
(h1 : F.cornerRadical x * F.cornerRadical x ≤ V)
(h2 : V ≤ F.cornerRadical x)
:
F.IsEndpointSubbimodule x x V
Subspaces between (rad R_x)² and rad R_x are ideals of R_x.
theorem
MultiplicativeBasisDeformations.PrimitiveIdempotents.exists_rad_gen
{k : Type u}
[Field k]
[IsAlgClosed k]
{A : Type v}
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
(F : PrimitiveIdempotents A)
(hA : IsRepresentationFinite k A)
(x : Fin F.m)
:
∃ t ∈ F.cornerRadical x, F.cornerRadical x ≤ k ∙ t ⊔ F.cornerRadical x * F.cornerRadical x
rad R_x / (rad R_x)² has dimension at most one.
theorem
MultiplicativeBasisDeformations.PrimitiveIdempotents.rad_le_endpointSpan
{k : Type u}
[Field k]
[IsAlgClosed k]
{A : Type v}
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
(F : PrimitiveIdempotents A)
(x : Fin F.m)
{t : A}
(ht : t ∈ F.cornerRadical x)
(hgen : F.cornerRadical x ≤ k ∙ t ⊔ F.cornerRadical x * F.cornerRadical x)
:
F.cornerRadical x ≤ F.endpointSpan x x t
rad R_x ⊆ R_x t R_x by Nakayama's lemma.
theorem
MultiplicativeBasisDeformations.PrimitiveIdempotents.exists_of_mem_span_left
{k : Type u}
[Field k]
[IsAlgClosed k]
{A : Type v}
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
(F : PrimitiveIdempotents A)
{x : Fin F.m}
{t z : A}
(hz : z ∈ Submodule.span k {g : A | ∃ a ∈ F.corner x x, g = a * t})
:
∃ a ∈ F.corner x x, z = a * t
theorem
MultiplicativeBasisDeformations.PrimitiveIdempotents.exists_of_mem_span_right
{k : Type u}
[Field k]
[IsAlgClosed k]
{A : Type v}
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
(F : PrimitiveIdempotents A)
{y : Fin F.m}
{t z : A}
(hz : z ∈ Submodule.span k {g : A | ∃ b ∈ F.corner y y, g = t * b})
:
∃ b ∈ F.corner y y, z = t * b
theorem
MultiplicativeBasisDeformations.PrimitiveIdempotents.cornerVal_mem_corner
{k : Type u}
[Field k]
[IsAlgClosed k]
{A : Type v}
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
(F : PrimitiveIdempotents A)
(x : Fin F.m)
(r : ⋯.Corner)
:
theorem
MultiplicativeBasisDeformations.PrimitiveIdempotents.cornerVal_algebraMap
{k : Type u}
[Field k]
[IsAlgClosed k]
{A : Type v}
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
(F : PrimitiveIdempotents A)
(x : Fin F.m)
(c : k)
:
theorem
MultiplicativeBasisDeformations.PrimitiveIdempotents.exists_aeval_surjective
(k : Type u)
[Field k]
[IsAlgClosed k]
{A : Type v}
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
(F : PrimitiveIdempotents A)
(hA : IsRepresentationFinite k A)
(x : Fin F.m)
:
∃ (t : ⋯.Corner), IsNilpotent t ∧ Function.Surjective ⇑(Polynomial.aeval t)
R_x is generated by one nilpotent element.
theorem
MultiplicativeBasisDeformations.PrimitiveIdempotents.localCorner_iso
(k : Type u)
[Field k]
[IsAlgClosed k]
{A : Type v}
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
(F : PrimitiveIdempotents A)
(hA : IsRepresentationFinite k A)
(x : Fin F.m)
:
∃ (N : ℕ), 1 ≤ N ∧ Nonempty (⋯.Corner ≃ₐ[k] Polynomial k ⧸ Ideal.span {Polynomial.X ^ N})
Lemma 3.1(2): R_x ≅ k[t]/(t^N) with N ≥ 1.