Lemma 6.6, the additional gradings #
lem:square-zero-selected-lifts (positive-deformations.tex), last sentence: "If Λ and
the M_i carry an additional grading by an abelian group, preserved by the multiplication and the
actions, and μ is homogeneous for it, then all these choices may be made homogeneous for this
grading."
For a grading by an arbitrary abelian group Γ (GrΓ, gradings of the modules compatible with
the actions; exists_actLiftΓ, ActLift.exists_isoΓ, exists_mapLiftΓ, through
WeightExtGroup.lean), and also for finitely many additional ℤ-gradings (GΛw i, MMw i, NNw i; e.g. the coordinates of the
integer weights of Section 7), compatible with the actions and the internal degree as in
WeightExt.lean, and μ of weight χ i for each: the lifted actions can be chosen of weight χ
(exists_actLiftW), two such lifts differ by a coordinate change of weight χ
(ActLift.exists_isoW), and a map of weight ω lifts with correction of weight ω + χ
(exists_mapLiftW). The corrections are the weight components of WeightExt.lean
(extVanish_weights1, extVanish_weights0).
theorem
MultiplicativeBasisDeformations.GExt.Good.one_deg
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{M : Type u_3}
{N : Type u_4}
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{GΛ' : GAlg Λ}
{MM' : GMod GΛ' M}
{NN' : GMod GΛ' N}
{t : ℤ}
{F : Bar.Cochain Λ (M →ₗ[R] N)}
(hF : Good MM' NN' 1 t F)
{u v : ℤ}
{m : M}
{a : Λ}
(hm : MM'.gr.IsHom u m)
(ha : GΛ'.gr.IsHom v a)
:
The degree of a weight-good one-cochain on homogeneous inputs.
theorem
MultiplicativeBasisDeformations.GExt.muCochain_goodW
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{MM : GMod GΛ M}
{r : ℕ}
{GΛw : Fin r → GAlg Λ}
(MMw : (i : Fin r) → GMod (GΛw i) M)
(hMa : ∀ (i : Fin r), (MMw i).act = MM.act)
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{χ : Fin r → ℤ}
(hχ : ∀ (i : Fin r), HDeg (GΛw i) μ (χ i))
(i : Fin r)
:
theorem
MultiplicativeBasisDeformations.GExt.exists_actLiftW
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{MM : GMod GΛ M}
{r : ℕ}
{GΛw : Fin r → GAlg Λ}
(MMw : (i : Fin r) → GMod (GΛw i) M)
(hMa : ∀ (i : Fin r), (MMw i).act = MM.act)
(hΛ : ∀ (i : Fin r) (v p : ℤ) (a : Λ), GΛ.gr.IsHom p a → GΛ.gr.IsHom p (((GΛw i).gr.proj v) a))
(hMp : ∀ (i : Fin r) (u p : ℤ) (m : M), MM.gr.IsHom p m → MM.gr.IsHom p (((MMw i).gr.proj u) m))
(hΛw : ∀ (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))
(hMw : ∀ (i j : Fin r) (u p : ℤ) (m : M), (MMw j).gr.IsHom p m → (MMw j).gr.IsHom p (((MMw i).gr.proj u) m))
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{q : ℤ}
(hq : HDeg GΛ μ q)
(hμ : IsHCocycle μ)
(h : ExtVanish MM MM 1 q)
{χ : Fin r → ℤ}
(hχ : ∀ (i : Fin r), HDeg (GΛw i) μ (χ i))
:
Lifted actions of weight χ.
theorem
MultiplicativeBasisDeformations.GExt.ActLift.act_degW
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{MM : GMod GΛ M}
{r : ℕ}
{GΛw : Fin r → GAlg Λ}
(MMw : (i : Fin r) → GMod (GΛw i) M)
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{q : ℤ}
(L : ActLift μ q MM)
{χ : Fin r → ℤ}
(hL : ∀ (i : Fin r), Good (MMw i) (MMw i) 1 (χ i) L.ν)
(i : Fin r)
{u v : ℤ}
{m : M}
{a : Λ}
(hm : (MMw i).gr.IsHom u m)
(ha : (GΛw i).gr.IsHom v a)
:
A lifted action of weight χ raises the weight by χ.
theorem
MultiplicativeBasisDeformations.GExt.ActLift.exists_isoW
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{MM : GMod GΛ M}
{r : ℕ}
{GΛw : Fin r → GAlg Λ}
(MMw : (i : Fin r) → GMod (GΛw i) M)
(hMa : ∀ (i : Fin r), (MMw i).act = MM.act)
(hMp : ∀ (i : Fin r) (u p : ℤ) (m : M), MM.gr.IsHom p m → MM.gr.IsHom p (((MMw i).gr.proj u) m))
(hMw : ∀ (i j : Fin r) (u p : ℤ) (m : M), (MMw j).gr.IsHom p m → (MMw j).gr.IsHom p (((MMw i).gr.proj u) m))
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{q : ℤ}
(L L' : ActLift μ q MM)
{χ : Fin r → ℤ}
(hL : ∀ (i : Fin r), Good (MMw i) (MMw i) 1 (χ i) L.ν)
(hL' : ∀ (i : Fin r), Good (MMw i) (MMw i) 1 (χ i) L'.ν)
(h : ExtVanish MM MM 0 q)
:
Uniqueness of weight-χ lifts up to a coordinate change 1 + εh of degree q and
weight χ.
theorem
MultiplicativeBasisDeformations.GExt.exists_mapLiftW
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{M : Type u_3}
{N : Type u_4}
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{MM : GMod GΛ M}
{NN : GMod GΛ N}
{r : ℕ}
{GΛw : Fin r → GAlg Λ}
(MMw : (i : Fin r) → GMod (GΛw i) M)
(NNw : (i : Fin r) → GMod (GΛw i) N)
(hMa : ∀ (i : Fin r), (MMw i).act = MM.act)
(hNa : ∀ (i : Fin r), (NNw i).act = NN.act)
(hMp : ∀ (i : Fin r) (u p : ℤ) (m : M), MM.gr.IsHom p m → MM.gr.IsHom p (((MMw i).gr.proj u) m))
(hNp : ∀ (i : Fin r) (x p : ℤ) (n : N), NN.gr.IsHom p n → NN.gr.IsHom p (((NNw i).gr.proj x) n))
(hMw : ∀ (i j : Fin r) (u p : ℤ) (m : M), (MMw j).gr.IsHom p m → (MMw j).gr.IsHom p (((MMw i).gr.proj u) m))
(hNw : ∀ (i j : Fin r) (x p : ℤ) (n : N), (NNw j).gr.IsHom p n → (NNw j).gr.IsHom p (((NNw i).gr.proj x) n))
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{q s : ℤ}
(L : ActLift μ q MM)
(L' : ActLift μ q NN)
{χ : Fin r → ℤ}
(hL : ∀ (i : Fin r), Good (MMw i) (MMw i) 1 (χ i) L.ν)
(hL' : ∀ (i : Fin r), Good (NNw i) (NNw i) 1 (χ i) L'.ν)
(f : M →ₗ[R] N)
(hf : ∀ (m : M) (a : Λ), f ((MM.act m) a) = (NN.act (f m)) a)
(hfdeg : ∀ (p : ℤ) (m : M), MM.gr.IsHom p m → NN.gr.IsHom (p + s) (f m))
{ω : Fin r → ℤ}
(hfw : ∀ (i : Fin r) (u : ℤ) (m : M), (MMw i).gr.IsHom u m → (NNw i).gr.IsHom (u + ω i) (f m))
(h : ExtVanish MM NN 0 (s + q))
:
Lifts of maps of weight ω with corrections of weight ω + χ.
A grading by an arbitrary abelian group #
theorem
MultiplicativeBasisDeformations.GExt.muCochain_goodΓ
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{MM : GMod GΛ M}
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{Γ : Type u_5}
[AddCommGroup Γ]
[DecidableEq Γ]
(gΛ : GrΓ Λ Γ)
(gM : MGr R Γ M)
(hMa' : ∀ (u v : Γ) (m : M) (a : Λ), gM.IsHom u m → gΛ.g.IsHom v a → gM.IsHom (u + v) ((MM.act m) a))
{χ : Γ}
(hχ : HDegΓ gΛ χ)
:
theorem
MultiplicativeBasisDeformations.GExt.exists_actLiftΓ
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{MM : GMod GΛ M}
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{Γ : Type u_5}
[AddCommGroup Γ]
[DecidableEq Γ]
(gΛ : GrΓ Λ Γ)
(gM : MGr R Γ M)
(hMa' : ∀ (u v : Γ) (m : M) (a : Λ), gM.IsHom u m → gΛ.g.IsHom v a → gM.IsHom (u + v) ((MM.act m) a))
(hΛ' : ∀ (v : Γ) (p : ℤ) (a : Λ), GΛ.gr.IsHom p a → GΛ.gr.IsHom p ((gΛ.g.proj v) a))
(hMp' : ∀ (u : Γ) (p : ℤ) (m : M), MM.gr.IsHom p m → MM.gr.IsHom p ((gM.proj u) m))
{q : ℤ}
(hq : HDeg GΛ μ q)
(hμ : IsHCocycle μ)
(h : ExtVanish MM MM 1 q)
{χ : Γ}
(hχ : HDegΓ gΛ χ)
:
Lemma 6.6, the lifted actions homogeneous for a grading by an abelian group.
theorem
MultiplicativeBasisDeformations.GExt.ActLift.exists_isoΓ
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{MM : GMod GΛ M}
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{Γ : Type u_5}
[AddCommGroup Γ]
[DecidableEq Γ]
(gΛ : GrΓ Λ Γ)
(gM : MGr R Γ M)
(hMa' : ∀ (u v : Γ) (m : M) (a : Λ), gM.IsHom u m → gΛ.g.IsHom v a → gM.IsHom (u + v) ((MM.act m) a))
(hMp' : ∀ (u : Γ) (p : ℤ) (m : M), MM.gr.IsHom p m → MM.gr.IsHom p ((gM.proj u) m))
{q : ℤ}
(L L' : ActLift μ q MM)
{χ : Γ}
(hL : GoodΓ gΛ gM gM 1 χ L.ν)
(hL' : GoodΓ gΛ gM gM 1 χ L'.ν)
(h : ExtVanish MM MM 0 q)
:
Lemma 6.6, uniqueness of Γ-homogeneous lifts up to a coordinate change of weight χ.
theorem
MultiplicativeBasisDeformations.GExt.exists_mapLiftΓ
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{M : Type u_3}
{N : Type u_4}
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{MM : GMod GΛ M}
{NN : GMod GΛ N}
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{Γ : Type u_5}
[AddCommGroup Γ]
[DecidableEq Γ]
(gΛ : GrΓ Λ Γ)
(gM : MGr R Γ M)
(gN : MGr R Γ N)
(hMa' : ∀ (u v : Γ) (m : M) (a : Λ), gM.IsHom u m → gΛ.g.IsHom v a → gM.IsHom (u + v) ((MM.act m) a))
(hNa' : ∀ (u v : Γ) (n : N) (a : Λ), gN.IsHom u n → gΛ.g.IsHom v a → gN.IsHom (u + v) ((NN.act n) a))
(hMp' : ∀ (u : Γ) (p : ℤ) (m : M), MM.gr.IsHom p m → MM.gr.IsHom p ((gM.proj u) m))
(hNp' : ∀ (x : Γ) (p : ℤ) (n : N), NN.gr.IsHom p n → NN.gr.IsHom p ((gN.proj x) n))
{q s : ℤ}
(L : ActLift μ q MM)
(L' : ActLift μ q NN)
{χ : Γ}
(hL : GoodΓ gΛ gM gM 1 χ L.ν)
(hL' : GoodΓ gΛ gN gN 1 χ L'.ν)
(f : M →ₗ[R] N)
(hf : ∀ (m : M) (a : Λ), f ((MM.act m) a) = (NN.act (f m)) a)
(hfdeg : ∀ (p : ℤ) (m : M), MM.gr.IsHom p m → NN.gr.IsHom (p + s) (f m))
{ω : Γ}
(hfw : ∀ (u : Γ) (m : M), gM.IsHom u m → gN.IsHom (u + ω) (f m))
(h : ExtVanish MM NN 0 (s + q))
:
Lemma 6.6, lifts of maps of Γ-weight ω with corrections of weight ω + χ.