Multiplicative bases

MultiplicativeBasisDeformations.Foundations.RayDegree

The radical degree of a ray #

Lemma 3.7 (projective-rays.tex). Write F^d A(x,y) for the radical filtration of a corner (F^0 = A(x,y), F^d = A(x,y) ∩ (rad A)^d). "Every F^dV is one of these submodules. Since endpoint radicals belong to J, F^dV = U_i ⟹ U_{i+1} ⊆ F^{d+1}V ⊆ U_i. Thus the filtration stays at a layer or drops to its successor […]. The rays are U_i ∖ U_{i+1}."

Here: each F^dV ≠ 0 is U(g) with R(g) ⊆ F^{d+1}V (radFilt_cyclic), so the graded pieces have dimension at most one (finrank_radFilt_le), elements of the same degree lie in the same ray (ray_eq_of_degree), and a strictly smaller subbimodule has a strictly larger degree (degree_lt_of_lt). The pieces F^dV/F^{d+1}V are the graded pieces A₀(x,y)_d of gr_J on projectives.

source
def MultiplicativeBasisDeformations.radFilt (k : Type u) [Field k] (A : Type v) [Ring A] [Algebra k A] :
ℕ → Submodule k A

The radical filtration: F^0 = A, F^d = (rad A)^d.

Instances For
    source
    theorem MultiplicativeBasisDeformations.radFilt_mul_left {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] (d : ℕ) (a : A) {z : A} (hz : z ∈ radFilt k A d) :
    a * z ∈ radFilt k A d
    source
    theorem MultiplicativeBasisDeformations.radFilt_mul_right {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] (d : ℕ) (a : A) {z : A} (hz : z ∈ radFilt k A d) :
    z * a ∈ radFilt k A d
    source
    theorem MultiplicativeBasisDeformations.rad_mul_radFilt {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] (d : ℕ) {a z : A} (ha : a ∈ algebraRadical k A) (hz : z ∈ radFilt k A d) :
    a * z ∈ radFilt k A (d + 1)
    source
    theorem MultiplicativeBasisDeformations.radFilt_mul_rad {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] (d : ℕ) {a z : A} (ha : a ∈ algebraRadical k A) (hz : z ∈ radFilt k A d) :
    z * a ∈ radFilt k A (d + 1)
    source
    theorem MultiplicativeBasisDeformations.radFilt_succ_le {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] (d : ℕ) :
    radFilt k A (d + 1) ≤ radFilt k A d
    source
    theorem MultiplicativeBasisDeformations.radFilt_antitone {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] {d d' : ℕ} (h : d ≤ d') :
    radFilt k A d' ≤ radFilt k A d
    source
    theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.radFilt_isEndpoint {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] [IsAlgClosed k] [FiniteDimensional k A] (F : PrimitiveIdempotents A) (x y : Fin F.m) (d : ℕ) :
    F.IsEndpointSubbimodule x y (F.corner x y ⊓ radFilt k A d)
    source
    theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.endpointRadical_le_radFilt {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] [IsAlgClosed k] [FiniteDimensional k A] (F : PrimitiveIdempotents A) {x y : Fin F.m} {g : A} (hg : g ∈ F.corner x y) {d : ℕ} (hgd : g ∈ radFilt k A d) :
    F.endpointRadical x y g ≤ F.corner x y ⊓ radFilt k A (d + 1)

    R(g) ⊆ F^{d+1} for g ∈ F^d: endpoint radicals belong to J.

    source
    theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.finrank_radFilt_le {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] [IsAlgClosed k] [FiniteDimensional k A] (F : PrimitiveIdempotents A) (hA : IsRepresentationFinite k A) (x y : Fin F.m) (d : ℕ) :
    Module.finrank k ↥(F.corner x y ⊓ radFilt k A d) ≤ Module.finrank k ↥(F.corner x y ⊓ radFilt k A (d + 1)) + 1

    Each graded piece of the radical filtration of a corner has dimension at most one.

    source
    theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.ray_eq_of_degree {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] [IsAlgClosed k] [FiniteDimensional k A] (F : PrimitiveIdempotents A) (hA : IsRepresentationFinite k A) {x y : Fin F.m} {f g : A} (hf : f ∈ F.corner x y) (hg : g ∈ F.corner x y) {d : ℕ} (hfd : f ∈ radFilt k A d) (hfd' : f ∉ radFilt k A (d + 1)) (hgd : g ∈ radFilt k A d) (hgd' : g ∉ radFilt k A (d + 1)) :
    F.ray x y f = F.ray x y g

    Elements of the same radical degree lie in the same ray.

    source
    theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.degree_lt_of_lt {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] [IsAlgClosed k] [FiniteDimensional k A] (F : PrimitiveIdempotents A) (hA : IsRepresentationFinite k A) {x y : Fin F.m} {f g : A} (hf : f ∈ F.corner x y) (hg : g ∈ F.corner x y) (hlt : F.endpointSpan x y g < F.endpointSpan x y f) {d d' : ℕ} (hfd : f ∈ radFilt k A d) (hgd' : g ∈ radFilt k A d') (hgd'' : g ∉ radFilt k A (d' + 1)) :
    d < d'

    A strictly smaller subbimodule has a strictly larger radical degree.

    source
    theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.exists_degree {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] [IsAlgClosed k] [FiniteDimensional k A] {f : A} (hf0 : f ≠ 0) :
    ∃ (d : ℕ), f ∈ radFilt k A d ∧ f ∉ radFilt k A (d + 1)

    Every nonzero element has a radical degree.