Weight-homogeneous lifts (Proposition 10.1, weight refinement)

integral-deformations.tex: "All these constructions can be chosen to preserve the simultaneous integer weights: […] the corrections can be chosen in each weight component."

Given finitely many integer weight gradings on Λ = A⁽²⁾, Λ' = A⁽⁴⁾ and a module M, compatible with the reduction, the action, the homogeneous bases and the internal degree, the module lift of exists_liftMod can be chosen with an action homogeneous for every weight (exists_liftMod_weights), and the arrow lifts of exists_liftHom homogeneous for every weight (exists_liftHom_weights). The corrections come from extVanish_weights1 and extVanish_weights0; the arbitrary lifts through homogeneous bases are homogeneous for every weight by the same computation as for the degree.

def MultiplicativeBasisDeformations.WLift.regrade {R : Type u_3} [CommRing R] {Λ : Type u_4} [Ring Λ] [Algebra R Λ] {GΛ GΛ₁ : GExt.GAlg Λ} {M : Type u_5} [AddCommGroup M] [Module R M] (MM : GExt.GMod GΛ M) (g : GExt.ZGr M) (hg : ∀ (p q : ℤ) (m : M) (a : Λ), g.IsHom p m → GΛ₁.gr.IsHom q a → g.IsHom (p + q) ((MM.act m) a)) : GExt.GMod GΛ₁ M

A module with another grading of the same algebra, compatible with the action.

theorem MultiplicativeBasisDeformations.WLift.exists_liftMod_weights {Λ : Type u_1} [Ring Λ] [Algebra (ZMod 2) Λ] {GΛ : GExt.GAlg Λ} {Λ' : Type u_2} [Ring Λ'] [Algebra (ZMod 4) Λ'] {GΛ' : GExt.GAlg Λ'} {π : Λ' →+* Λ} {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (β : Module.Basis ι (ZMod 2) M) (dβ : ι → ℤ) {MM : GExt.GMod GΛ M} {κ : Type u_5} [Fintype κ] (bΛ : Module.Basis κ (ZMod 4) Λ') (hπ : IsRed GΛ' GΛ π) (dΛ : κ → ℤ) (hbΛ : ∀ (κ' : κ), GΛ'.gr.IsHom (dΛ κ') (bΛ κ')) (hβ : ∀ (i : ι), MM.gr.IsHom (dβ i) (β i)) {r : ℕ} {GΛw : Fin r → GExt.GAlg Λ} {GΛ'w : Fin r → GExt.GAlg Λ'} (hπw : ∀ (i : Fin r), IsRed (GΛ'w i) (GΛw i) π) (gw : Fin r → GExt.ZGr M) (hgw : ∀ (i : Fin r) (p q : ℤ) (m : M) (a : Λ), (gw i).IsHom p m → (GΛw i).gr.IsHom q a → (gw i).IsHom (p + q) ((MM.act m) a)) (wβ : Fin r → ι → ℤ) (hβw : ∀ (i : Fin r) (j : ι), (gw i).IsHom (wβ i j) (β j)) (wΛ : Fin r → κ → ℤ) (hbΛw : ∀ (i : Fin r) (κ' : κ), (GΛ'w i).gr.IsHom (wΛ i κ') (bΛ κ')) (hΛc : ∀ (i : Fin r) (v p : ℤ) (a : Λ), GΛ.gr.IsHom p a → GΛ.gr.IsHom p (((GΛw i).gr.proj v) a)) (hMc : ∀ (i : Fin r) (u p : ℤ) (m : M), MM.gr.IsHom p m → MM.gr.IsHom p (((gw i).proj u) m)) (hΛcw : ∀ (i j : Fin r) (v p : ℤ) (a : Λ), (GΛw j).gr.IsHom p a → (GΛw j).gr.IsHom p (((GΛw i).gr.proj v) a)) (hMcw : ∀ (i j : Fin r) (u p : ℤ) (m : M), (gw j).IsHom p m → (gw j).IsHom p (((gw i).proj u) m)) (hExt : GExt.ExtVanish MM MM 1 0) : ∃ (MM' : GExt.GMod GΛ' (ι → ZMod 4)), IsLift MM' MM π (ρF β) ∧ MM'.gr = grF dβ ∧ ∀ (i : Fin r) (p q : ℤ) (m : ι → ZMod 4) (a : Λ'), (grF (wβ i)).IsHom p m → (GΛ'w i).gr.IsHom q a → (grF (wβ i)).IsHom (p + q) ((MM'.act m) a)

Proposition 10.1, the module lifts, weight-homogeneous: the lifted action can be chosen homogeneous for every weight.

Weight-homogeneous arrow lifts

theorem MultiplicativeBasisDeformations.WLift.exists_liftHom_weights {Λ : Type u_1} [Ring Λ] [Algebra (ZMod 2) Λ] {GΛ : GExt.GAlg Λ} {Λ' : Type u_2} [Ring Λ'] [Algebra (ZMod 4) Λ'] {GΛ' : GExt.GAlg Λ'} {π : Λ' →+* Λ} {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {M' : Type u_4} [AddCommGroup M'] [Module (ZMod 4) M'] {MM' : GExt.GMod GΛ' M'} {MM : GExt.GMod GΛ M} {ρM : M' →+ M} {N : Type u_5} [AddCommGroup N] [Module (ZMod 2) N] {N' : Type u_6} [AddCommGroup N'] [Module (ZMod 4) N'] {NN' : GExt.GMod GΛ' N'} {NN : GExt.GMod GΛ N} {ρN : N' →+ N} (hπ : IsRed GΛ' GΛ π) (HM : IsLift MM' MM π ρM) (HN : IsLift NN' NN π ρN) {r : ℕ} {GΛw : Fin r → GExt.GAlg Λ} {GΛ'w : Fin r → GExt.GAlg Λ'} (hπw : ∀ (i : Fin r), IsRed (GΛ'w i) (GΛw i) π) (gM : Fin r → GExt.ZGr M) (hgM : ∀ (i : Fin r) (p q : ℤ) (m : M) (a : Λ), (gM i).IsHom p m → (GΛw i).gr.IsHom q a → (gM i).IsHom (p + q) ((MM.act m) a)) (gN : Fin r → GExt.ZGr N) (hgN : ∀ (i : Fin r) (p q : ℤ) (n : N) (a : Λ), (gN i).IsHom p n → (GΛw i).gr.IsHom q a → (gN i).IsHom (p + q) ((NN.act n) a)) (gM' : Fin r → GExt.ZGr M') (hgM' : ∀ (i : Fin r) (p q : ℤ) (m : M') (a : Λ'), (gM' i).IsHom p m → (GΛ'w i).gr.IsHom q a → (gM' i).IsHom (p + q) ((MM'.act m) a)) (gN' : Fin r → GExt.ZGr N') (hgN' : ∀ (i : Fin r) (p q : ℤ) (n : N') (a : Λ'), (gN' i).IsHom p n → (GΛ'w i).gr.IsHom q a → (gN' i).IsHom (p + q) ((NN'.act n) a)) (HMw : ∀ (i : Fin r), IsLift (regrade MM' (gM' i) ⋯) (regrade MM (gM i) ⋯) π ρM) (HNw : ∀ (i : Fin r), IsLift (regrade NN' (gN' i) ⋯) (regrade NN (gN i) ⋯) π ρN) (hMc : ∀ (i : Fin r) (u p : ℤ) (m : M), MM.gr.IsHom p m → MM.gr.IsHom p (((gM i).proj u) m)) (hNc : ∀ (i : Fin r) (x p : ℤ) (n : N), NN.gr.IsHom p n → NN.gr.IsHom p (((gN i).proj x) n)) (hMcw : ∀ (i j : Fin r) (u p : ℤ) (m : M), (gM j).IsHom p m → (gM j).IsHom p (((gM i).proj u) m)) (hNcw : ∀ (i j : Fin r) (x p : ℤ) (n : N), (gN j).IsHom p n → (gN j).IsHom p (((gN i).proj x) n)) (f : M →ₗ[ZMod 2] N) (hf : ∀ (m : M) (a : Λ), f ((MM.act m) a) = (NN.act (f m)) a) {d : ℤ} (e : Fin r → ℤ) (hExt : GExt.ExtVanish MM NN 0 d) (f₀ : M' →ₗ[ZMod 4] N') (hf₀ : ∀ (m : M'), ρN (f₀ m) = f (ρM m)) (hf₀d : ∀ (p : ℤ) (m : M'), MM'.gr.IsHom p m → NN'.gr.IsHom (p + d) (f₀ m)) (hf₀w : ∀ (i : Fin r) (p : ℤ) (m : M'), (gM' i).IsHom p m → (gN' i).IsHom (p + e i) (f₀ m)) : ∃ (f' : M' →ₗ[ZMod 4] N'), (∀ (m : M') (b : Λ'), f' ((MM'.act m) b) = (NN'.act (f' m)) b) ∧ (∀ (m : M'), ρN (f' m) = f (ρM m)) ∧ (∀ (p : ℤ) (m : M'), MM'.gr.IsHom p m → NN'.gr.IsHom (p + d) (f' m)) ∧ ∀ (i : Fin r) (p : ℤ) (m : M'), (gM' i).IsHom p m → (gN' i).IsHom (p + e i) (f' m)

Proposition 10.1, the arrow lifts, weight-homogeneous: a map homogeneous of degree d and of weights e i, with a lift f₀ of the same degree and weights, has a lift with the same degree and weights.