Proposition 6.5(3): regular lifts at projective labels

positive-deformations.tex: "If M_i = e_xΛ for a primitive idempotent e_x of Λ₀, we may choose M_i^B = e_xB for a lift e_x ∈ B of that idempotent. […] At a projective label, the actual regular module e_xB has the required associated grading."

We give eΛ (e of degree zero) its graded right module structure (rightIdeal), and show that the regular module e B, identified with eΛ through a splitting φ multiplicative on the left by e (Lemma 6.4), is a filtered lift of eΛ (regularLift). By the uniqueness of Proposition 6.5(1) it is then isomorphic to any other filtered lift.

theorem MultiplicativeBasisDeformations.LenGrading.proj_mul_left {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] (G : LenGrading k Λ) {e : Λ} (he : G.IsHom 0 e) (d : ℕ) (a : Λ) : (G.proj d) (e * a) = e * (G.proj d) a

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.GExt.RI (k : Type u) [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] (e : Λ) : Submodule k Λ

The right ideal eΛ.

theorem MultiplicativeBasisDeformations.GExt.mem_RI {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {e : Λ} (hidem : IsIdempotentElem e) {x : Λ} : x ∈ RI k e ↔ e * x = x

theorem MultiplicativeBasisDeformations.GExt.proj_mem_RI {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {e : Λ} (he : G.IsHom 0 e) (hidem : IsIdempotentElem e) {x : Λ} (hx : x ∈ RI k e) (p : ℤ) : ((ZGr.ofLen G).proj p) x ∈ RI k e

def MultiplicativeBasisDeformations.GExt.riGr {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {e : Λ} (he : G.IsHom 0 e) (hidem : IsIdempotentElem e) : ZGr ↥(RI k e)

The grading of eΛ.

def MultiplicativeBasisDeformations.GExt.rightIdeal {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} (h1 : G.IsHom 0 1) {e : Λ} (he : G.IsHom 0 e) (hidem : IsIdempotentElem e) : GMod (GAlg.ofLen G h1) ↥(RI k e)

The graded right module eΛ.

theorem MultiplicativeBasisDeformations.PosFiltration.exists_split_left {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type w} [Ring B] [Algebra k B] (P : PosFiltration G B) (V : G.Vertices) : ∃ (S : P.Split), ∀ (i : Fin V.n) (a : Λ), S.φ (V.e i * a) = S.φ (V.e i) * S.φ a

Lemma 6.4 with the left S-linearity of the splitting.

def MultiplicativeBasisDeformations.PosFiltration.Split.regularLift {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type w} [Ring B] [Algebra k B] {P : PosFiltration G B} (h1 : G.IsHom 0 1) {e : Λ} (he : G.IsHom 0 e) (hidem : IsIdempotentElem e) (S : P.Split) (hleft : ∀ (a : Λ), S.φ (e * a) = S.φ e * S.φ a) : P.FLift h1 (GExt.rightIdeal h1 he hidem)

The regular module eB is a filtered lift of eΛ (Proposition 6.5(3), last sentence): its action, transported along the splitting, is m · y = φ⁻¹(φ(m) y).