Corrections in each weight component, for a grading by any abelian group #
The version of WeightExt.lean for an additional grading by an arbitrary abelian group Γ
(lem:square-zero-selected-lifts, last sentence): a Γ-grading of Λ (GrΓ), of the modules
(MGr compatible with the actions), and a correction H with dH = F for F of weight w
replaced by its weight-w component (PW0Γ, PW1Γ, dPW0Γ, dPW1Γ). The component is
computed on homogeneous inputs (PW0Γ_hom, PW1Γ_hom); cochains agreeing on homogeneous inputs
agree (ext_oneΓ, ext_twoΓ).
def
MultiplicativeBasisDeformations.GExt.GoodΓ
{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]
{Γ : Type u_5}
[AddCommGroup Γ]
[DecidableEq Γ]
(gΛ : GrΓ Λ Γ)
(gM : MGr R Γ M)
(gN : MGr R Γ N)
(n : ℕ)
(w : Γ)
(F : Bar.Cochain Λ (M →ₗ[R] N))
:
A Γ-homogeneous cochain of weight w (only the weights; the algebraic properties are those
of Good).
Instances For
def
MultiplicativeBasisDeformations.GExt.PW0Γ
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
{M : Type u_3}
{N : Type u_4}
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{Γ : Type u_5}
[AddCommGroup Γ]
[DecidableEq Γ]
(gM : MGr R Γ M)
(gN : MGr R Γ N)
(w : Γ)
(H : Bar.Cochain Λ (M →ₗ[R] N))
:
Bar.Cochain Λ (M →ₗ[R] N)
The weight-w component of a 0-cochain.
Instances For
def
MultiplicativeBasisDeformations.GExt.PW1Γ
{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]
{Γ : Type u_5}
[AddCommGroup Γ]
[DecidableEq Γ]
(gΛ : GrΓ Λ Γ)
(gM : MGr R Γ M)
(gN : MGr R Γ N)
(w : Γ)
(H : Bar.Cochain Λ (M →ₗ[R] N))
:
Bar.Cochain Λ (M →ₗ[R] N)
The weight-w component of a 1-cochain.
Instances For
theorem
MultiplicativeBasisDeformations.GExt.PW0Γ_hom
{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]
{Γ : Type u_5}
[AddCommGroup Γ]
[DecidableEq Γ]
(gM : MGr R Γ M)
(gN : MGr R Γ N)
(w : Γ)
(H : Bar.Cochain Λ (M →ₗ[R] N))
(a : ℕ → Λ)
{u₀ : Γ}
{m : M}
(hm : gM.IsHom u₀ m)
:
theorem
MultiplicativeBasisDeformations.GExt.PW1Γ_hom
{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]
{Γ : Type u_5}
[AddCommGroup Γ]
[DecidableEq Γ]
(gΛ : GrΓ Λ Γ)
(gM : MGr R Γ M)
(gN : MGr R Γ N)
{GΛo : GAlg Λ}
{MMo : GMod GΛo M}
{NNo : GMod GΛo N}
{t : ℤ}
(w : Γ)
{H : Bar.Cochain Λ (M →ₗ[R] N)}
(hH : Good MMo NNo 1 t H)
(a : ℕ → Λ)
{v₀ u₀ : Γ}
{m : M}
(ha : gΛ.g.IsHom v₀ (a 0))
(hm : gM.IsHom u₀ m)
:
theorem
MultiplicativeBasisDeformations.GExt.PW1Γ_good
{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]
{Γ : Type u_5}
[AddCommGroup Γ]
[DecidableEq Γ]
(gΛ : GrΓ Λ Γ)
(gM : MGr R Γ M)
(gN : MGr R Γ N)
{GΛo : GAlg Λ}
{MMo : GMod GΛo M}
{NNo : GMod GΛo N}
{t : ℤ}
(w : Γ)
{H : Bar.Cochain Λ (M →ₗ[R] N)}
(hH : Good MMo NNo 1 t H)
(hΛ : ∀ (v : Γ) (p : ℤ) (a : Λ), GΛo.gr.IsHom p a → GΛo.gr.IsHom p ((gΛ.g.proj v) a))
(hMp : ∀ (u : Γ) (p : ℤ) (m : M), MMo.gr.IsHom p m → MMo.gr.IsHom p ((gM.proj u) m))
(hNp : ∀ (x : Γ) (p : ℤ) (n : N), NNo.gr.IsHom p n → NNo.gr.IsHom p ((gN.proj x) n))
:
theorem
MultiplicativeBasisDeformations.GExt.PW1Γ_goodΓ
{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]
{Γ : Type u_5}
[AddCommGroup Γ]
[DecidableEq Γ]
(gΛ : GrΓ Λ Γ)
(gM : MGr R Γ M)
(gN : MGr R Γ N)
{GΛo : GAlg Λ}
{MMo : GMod GΛo M}
{NNo : GMod GΛo N}
{t : ℤ}
(w : Γ)
{H : Bar.Cochain Λ (M →ₗ[R] N)}
(hH : Good MMo NNo 1 t H)
:
theorem
MultiplicativeBasisDeformations.GExt.PW0Γ_good
{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]
{Γ : Type u_5}
[AddCommGroup Γ]
[DecidableEq Γ]
(gM : MGr R Γ M)
(gN : MGr R Γ N)
{GΛo : GAlg Λ}
{MMo : GMod GΛo M}
{NNo : GMod GΛo N}
{t : ℤ}
(w : Γ)
{H : Bar.Cochain Λ (M →ₗ[R] N)}
(hH : Good MMo NNo 0 t H)
(hMp : ∀ (u : Γ) (p : ℤ) (m : M), MMo.gr.IsHom p m → MMo.gr.IsHom p ((gM.proj u) m))
(hNp : ∀ (x : Γ) (p : ℤ) (n : N), NNo.gr.IsHom p n → NNo.gr.IsHom p ((gN.proj x) n))
:
theorem
MultiplicativeBasisDeformations.GExt.PW0Γ_goodΓ
{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]
{Γ : Type u_5}
[AddCommGroup Γ]
[DecidableEq Γ]
(gΛ : GrΓ Λ Γ)
(gM : MGr R Γ M)
(gN : MGr R Γ N)
(w : Γ)
(H : Bar.Cochain Λ (M →ₗ[R] N))
:
Agreement on homogeneous inputs #
theorem
MultiplicativeBasisDeformations.GExt.ext_oneΓ
{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]
{Γ : Type u_5}
[AddCommGroup Γ]
[DecidableEq Γ]
(gΛ : GrΓ Λ Γ)
(gM : MGr R Γ M)
{GΛo : GAlg Λ}
{MMo : GMod GΛo M}
{NNo : GMod GΛo N}
{t : ℤ}
{G G' : Bar.Cochain Λ (M →ₗ[R] N)}
(hG : Good MMo NNo 1 t G)
(hG' : Good MMo NNo 1 t G')
(h : ∀ (a : Λ) (m : M) (v u : Γ), gΛ.g.IsHom v a → gM.IsHom u m → (G (single a)) m = (G' (single a)) m)
:
G = G'
theorem
MultiplicativeBasisDeformations.GExt.ext_twoΓ
{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]
{Γ : Type u_5}
[AddCommGroup Γ]
[DecidableEq Γ]
(gΛ : GrΓ Λ Γ)
(gM : MGr R Γ M)
{GΛo : GAlg Λ}
{MMo : GMod GΛo M}
{NNo : GMod GΛo N}
{t : ℤ}
{G G' : Bar.Cochain Λ (M →ₗ[R] N)}
(hG : Good MMo NNo 2 t G)
(hG' : Good MMo NNo 2 t G')
(h :
∀ (a b : Λ) (m : M) (v₀ v₁ u : Γ),
gΛ.g.IsHom v₀ a → gΛ.g.IsHom v₁ b → gM.IsHom u m → (G (pair a b)) m = (G' (pair a b)) m)
:
G = G'
The corrections, weight by weight #
theorem
MultiplicativeBasisDeformations.GExt.proj_actΓ
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{N : Type u_4}
[AddCommGroup N]
[Module R N]
{Γ : Type u_5}
[AddCommGroup Γ]
[DecidableEq Γ]
(gΛ : GrΓ Λ Γ)
(gN : MGr R Γ N)
{GΛ : GAlg Λ}
{NN : GMod GΛ N}
(hNa : ∀ (u v : Γ) (n : N) (a : Λ), gN.IsHom u n → gΛ.g.IsHom v a → gN.IsHom (u + v) ((NN.act n) a))
{q : Γ}
{a : Λ}
(ha : gΛ.g.IsHom q a)
(p : Γ)
(y : N)
:
theorem
MultiplicativeBasisDeformations.GExt.dPW1Γ
{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]
{Γ : Type u_5}
[AddCommGroup Γ]
[DecidableEq Γ]
(gΛ : GrΓ Λ Γ)
(gM : MGr R Γ M)
(gN : MGr R Γ N)
{GΛ : GAlg Λ}
{MM : GMod GΛ M}
{NN : GMod GΛ 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))
(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))
(hNp : ∀ (x : Γ) (p : ℤ) (n : N), NN.gr.IsHom p n → NN.gr.IsHom p ((gN.proj x) n))
{t : ℤ}
{w : Γ}
{H : Bar.Cochain Λ (M →ₗ[R] N)}
(hH : Good MM NN 1 t H)
{F : Bar.Cochain Λ (M →ₗ[R] N)}
(hFw : GoodΓ gΛ gM gN 2 w F)
(hd : (Bar.d (homAct MM NN) 1) H = F)
:
d of the component of a 1-cochain is the given weight-w cocycle.
theorem
MultiplicativeBasisDeformations.GExt.dPW0Γ
{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]
{Γ : Type u_5}
[AddCommGroup Γ]
[DecidableEq Γ]
(gΛ : GrΓ Λ Γ)
(gM : MGr R Γ M)
(gN : MGr R Γ N)
{GΛ : GAlg Λ}
{MM : GMod GΛ M}
{NN : GMod GΛ 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))
{t : ℤ}
{w : Γ}
{H : Bar.Cochain Λ (M →ₗ[R] N)}
(hH : Good MM NN 0 t H)
{F : Bar.Cochain Λ (M →ₗ[R] N)}
(hFw : GoodΓ gΛ gM gN 1 w F)
(hd : (Bar.d (homAct MM NN) 0) H = F)
:
d of the component of a 0-cochain is the given weight-w cocycle.
theorem
MultiplicativeBasisDeformations.GExt.extVanishΓ1
{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]
{Γ : Type u_5}
[AddCommGroup Γ]
[DecidableEq Γ]
(gΛ : GrΓ Λ Γ)
(gM : MGr R Γ M)
(gN : MGr R Γ N)
{GΛ : GAlg Λ}
{MM : GMod GΛ M}
{NN : GMod GΛ 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))
(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))
(hNp : ∀ (x : Γ) (p : ℤ) (n : N), NN.gr.IsHom p n → NN.gr.IsHom p ((gN.proj x) n))
{t : ℤ}
(hExt : ExtVanish MM NN 1 t)
(w : Γ)
(F : Bar.Cochain Λ (M →ₗ[R] N))
(hF : Good MM NN 2 t F)
(hFw : GoodΓ gΛ gM gN 2 w F)
(hdF : (Bar.d (homAct MM NN) 2) F = 0)
:
∃ (H : Bar.Cochain Λ (M →ₗ[R] N)), Good MM NN 1 t H ∧ GoodΓ gΛ gM gN 1 w H ∧ (Bar.d (homAct MM NN) 1) H = F
Ext² corrections in a weight component of a Γ-grading.
theorem
MultiplicativeBasisDeformations.GExt.extVanishΓ0
{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]
{Γ : Type u_5}
[AddCommGroup Γ]
[DecidableEq Γ]
(gΛ : GrΓ Λ Γ)
(gM : MGr R Γ M)
(gN : MGr R Γ N)
{GΛ : GAlg Λ}
{MM : GMod GΛ M}
{NN : GMod GΛ 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))
{t : ℤ}
(hExt : ExtVanish MM NN 0 t)
(w : Γ)
(F : Bar.Cochain Λ (M →ₗ[R] N))
(hF : Good MM NN 1 t F)
(hFw : GoodΓ gΛ gM gN 1 w F)
(hdF : (Bar.d (homAct MM NN) 1) F = 0)
:
∃ (H : Bar.Cochain Λ (M →ₗ[R] N)), Good MM NN 0 t H ∧ GoodΓ gΛ gM gN 0 w H ∧ (Bar.d (homAct MM NN) 0) H = F
Ext¹ corrections in a weight component of a Γ-grading.