Corrections in each weight component (Proposition 10.1, last paragraph) #
integral-deformations.tex: "All these constructions can be chosen to preserve the
simultaneous integer weights: lifting a basis of H_ℤ to mesh weights by Lemma 7.4 gives the
modules M_i⁽²⁾ compatible weight gradings, and the corrections can be chosen in each weight
component."
A second ℤ-grading (a weight) on Λ, M, N, compatible with the same actions and commuting
with the internal degree, refines graded Ext: the corrections used in Proposition 10.1 come from
Ext¹ and Ext² (ExtVanish _ _ 0 _, ExtVanish _ _ 1 _), and a correction H with dH = F
can be replaced by its weight-w component PW w H when F has weight w (dPW0, dPW1).
The component is computed on homogeneous inputs, where it is the weight projection of the value;
two multilinear cochains agreeing on homogeneous inputs agree (ext_one, ext_two).
Several weights are treated one after another (extVanish_weights): each projection preserves the
degree and the earlier weights.
theorem
MultiplicativeBasisDeformations.GExt.ZGr.proj_sum_hom
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
(g : ZGr M)
{ι : Type u_3}
(s : Finset ι)
(x : ι → M)
(f : ι → ℤ)
(h : ∀ i ∈ s, g.IsHom (f i) (x i))
(w : ℤ)
:
(g.proj w) (∑ i ∈ s, x i) = ∑ i ∈ s with f i = w, x i
The projection of a sum of homogeneous terms.
def
MultiplicativeBasisDeformations.GExt.PW0
{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Λw : GAlg Λ}
(MMw : GMod GΛw M)
(NNw : GMod GΛw 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]
{GΛw : GAlg Λ}
(MMw : GMod GΛw M)
(NNw : GMod GΛw 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]
{GΛw : GAlg Λ}
(MMw : GMod GΛw M)
(NNw : GMod GΛw N)
(w : ℤ)
(H : Bar.Cochain Λ (M →ₗ[R] N))
(a : ℕ → Λ)
{u₀ : ℤ}
{m : M}
(hm : MMw.gr.IsHom u₀ m)
:
On a homogeneous input, the component of a 0-cochain is the projection of the value.
theorem
MultiplicativeBasisDeformations.GExt.single_zero_eq
{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Λo : GAlg Λ}
{MMo : GMod GΛo M}
{NNo : GMod GΛo N}
{t : ℤ}
{H : Bar.Cochain Λ (M →ₗ[R] N)}
(hH : Good MMo NNo 1 t H)
:
H (single 0) = 0
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]
{GΛw : GAlg Λ}
(MMw : GMod GΛw M)
(NNw : GMod GΛw 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Λw.gr.IsHom v₀ (a 0))
(hm : MMw.gr.IsHom u₀ m)
:
On homogeneous inputs, the component of a 1-cochain is the projection of the value.
theorem
MultiplicativeBasisDeformations.GExt.PW1_tr
{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Λw : GAlg Λ}
(MMw : GMod GΛw M)
(NNw : GMod GΛw N)
(w : ℤ)
(H : Bar.Cochain Λ (M →ₗ[R] N))
(a : ℕ → Λ)
:
theorem
MultiplicativeBasisDeformations.GExt.PW1_add
{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Λw : GAlg Λ}
(MMw : GMod GΛw M)
(NNw : GMod GΛw 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 : ℕ → Λ)
(x y : Λ)
:
theorem
MultiplicativeBasisDeformations.GExt.PW1_smul
{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Λw : GAlg Λ}
(MMw : GMod GΛw M)
(NNw : GMod GΛw 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 : ℕ → Λ)
(c : R)
(x : Λ)
:
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]
{GΛw : GAlg Λ}
(MMw : GMod GΛw M)
(NNw : GMod GΛw 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Λw.gr.proj v) a))
(hMp : ∀ (u p : ℤ) (m : M), MMo.gr.IsHom p m → MMo.gr.IsHom p ((MMw.gr.proj u) m))
(hNp : ∀ (x p : ℤ) (n : N), NNo.gr.IsHom p n → NNo.gr.IsHom p ((NNw.gr.proj x) n))
:
The component keeps every grading its projections preserve.
theorem
MultiplicativeBasisDeformations.GExt.PW1_goodW
{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Λw : GAlg Λ}
(MMw : GMod GΛw M)
(NNw : GMod GΛw 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)
:
The component is homogeneous of weight w.
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]
{GΛw : GAlg Λ}
(MMw : GMod GΛw M)
(NNw : GMod GΛw 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 ((MMw.gr.proj u) m))
(hNp : ∀ (x p : ℤ) (n : N), NNo.gr.IsHom p n → NNo.gr.IsHom p ((NNw.gr.proj x) n))
:
The 0-cochain version.
theorem
MultiplicativeBasisDeformations.GExt.PW0_goodW
{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Λw : GAlg Λ}
(MMw : GMod GΛw M)
(NNw : GMod GΛw 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)
:
Agreement on homogeneous inputs #
The sequence (a, b, 0, …).
Instances For
theorem
MultiplicativeBasisDeformations.GExt.Good.pair_eq
{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Λo : GAlg Λ}
{MMo : GMod GΛo M}
{NNo : GMod GΛo N}
{t : ℤ}
{G : Bar.Cochain Λ (M →ₗ[R] N)}
(hG : Good MMo NNo 2 t G)
(a : ℕ → Λ)
:
G a = G (pair (a 0) (a 1))
theorem
MultiplicativeBasisDeformations.GExt.Good.pair_add_left
{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Λo : GAlg Λ}
{MMo : GMod GΛo M}
{NNo : GMod GΛo N}
{t : ℤ}
{G : Bar.Cochain Λ (M →ₗ[R] N)}
(hG : Good MMo NNo 2 t G)
(x x' y : Λ)
:
theorem
MultiplicativeBasisDeformations.GExt.Good.pair_add_right
{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Λo : GAlg Λ}
{MMo : GMod GΛo M}
{NNo : GMod GΛo N}
{t : ℤ}
{G : Bar.Cochain Λ (M →ₗ[R] N)}
(hG : Good MMo NNo 2 t G)
(x y y' : Λ)
:
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]
{GΛw : GAlg Λ}
(MMw : GMod GΛw 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Λw.gr.IsHom v a → MMw.gr.IsHom u m → (G (single a)) m = (G' (single a)) m)
:
G = G'
1-cochains agreeing on homogeneous inputs agree.
theorem
MultiplicativeBasisDeformations.GExt.Good.pair_zero_left
{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Λo : GAlg Λ}
{MMo : GMod GΛo M}
{NNo : GMod GΛo N}
{t : ℤ}
{G : Bar.Cochain Λ (M →ₗ[R] N)}
(hG : Good MMo NNo 2 t G)
(y : Λ)
:
G (pair 0 y) = 0
theorem
MultiplicativeBasisDeformations.GExt.Good.pair_zero_right
{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Λo : GAlg Λ}
{MMo : GMod GΛo M}
{NNo : GMod GΛo N}
{t : ℤ}
{G : Bar.Cochain Λ (M →ₗ[R] N)}
(hG : Good MMo NNo 2 t G)
(x : Λ)
:
G (pair x 0) = 0
def
MultiplicativeBasisDeformations.GExt.bil
{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Λo : GAlg Λ}
{MMo : GMod GΛo M}
{NNo : GMod GΛo N}
{t : ℤ}
{G : Bar.Cochain Λ (M →ₗ[R] N)}
(hG : Good MMo NNo 2 t G)
:
Λ →+ Λ →+ M →ₗ[R] N
A good 2-cochain as a biadditive map.
Instances For
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]
{GΛw : GAlg Λ}
(MMw : GMod GΛw 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Λw.gr.IsHom v₀ a → GΛw.gr.IsHom v₁ b → MMw.gr.IsHom u m → (G (pair a b)) m = (G' (pair a b)) m)
:
G = G'
2-cochains agreeing on homogeneous inputs agree.
The corrections, weight by weight #
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]
{GΛ GΛw : GAlg Λ}
{MM : GMod GΛ M}
{NN : GMod GΛ N}
{MMw : GMod GΛw M}
{NNw : GMod GΛw N}
(hMa : MMw.act = MM.act)
(hNa : NNw.act = NN.act)
(hΛ : ∀ (v p : ℤ) (a : Λ), GΛ.gr.IsHom p a → GΛ.gr.IsHom p ((GΛw.gr.proj v) a))
(hMp : ∀ (u p : ℤ) (m : M), MM.gr.IsHom p m → MM.gr.IsHom p ((MMw.gr.proj u) m))
(hNp : ∀ (x p : ℤ) (n : N), NN.gr.IsHom p n → NN.gr.IsHom p ((NNw.gr.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 MMw NNw 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]
{GΛ GΛw : GAlg Λ}
{MM : GMod GΛ M}
{NN : GMod GΛ N}
{MMw : GMod GΛw M}
{NNw : GMod GΛw N}
(hMa : MMw.act = MM.act)
(hNa : NNw.act = NN.act)
(hMp : ∀ (u p : ℤ) (m : M), MM.gr.IsHom p m → MM.gr.IsHom p ((MMw.gr.proj u) m))
(hNp : ∀ (x p : ℤ) (n : N), NN.gr.IsHom p n → NN.gr.IsHom p ((NNw.gr.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 MMw NNw 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_weight1
{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Λ GΛw : GAlg Λ}
{MM : GMod GΛ M}
{NN : GMod GΛ N}
{MMw : GMod GΛw M}
{NNw : GMod GΛw N}
(hMa : MMw.act = MM.act)
(hNa : NNw.act = NN.act)
(hΛ : ∀ (v p : ℤ) (a : Λ), GΛ.gr.IsHom p a → GΛ.gr.IsHom p ((GΛw.gr.proj v) a))
(hMp : ∀ (u p : ℤ) (m : M), MM.gr.IsHom p m → MM.gr.IsHom p ((MMw.gr.proj u) m))
(hNp : ∀ (x p : ℤ) (n : N), NN.gr.IsHom p n → NN.gr.IsHom p ((NNw.gr.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 MMw NNw 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 MMw NNw 1 w H ∧ (Bar.d (homAct MM NN) 1) H = F
Ext² corrections in a weight component.
theorem
MultiplicativeBasisDeformations.GExt.extVanish_weight0
{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Λ GΛw : GAlg Λ}
{MM : GMod GΛ M}
{NN : GMod GΛ N}
{MMw : GMod GΛw M}
{NNw : GMod GΛw N}
(hMa : MMw.act = MM.act)
(hNa : NNw.act = NN.act)
(hMp : ∀ (u p : ℤ) (m : M), MM.gr.IsHom p m → MM.gr.IsHom p ((MMw.gr.proj u) m))
(hNp : ∀ (x p : ℤ) (n : N), NN.gr.IsHom p n → NN.gr.IsHom p ((NNw.gr.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 MMw NNw 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 MMw NNw 0 w H ∧ (Bar.d (homAct MM NN) 0) H = F
Ext¹ corrections in a weight component.
Several weights #
def
MultiplicativeBasisDeformations.GExt.seq1
{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]
{r : ℕ}
{GΛw : Fin r → GAlg Λ}
(MMw : (i : Fin r) → GMod (GΛw i) M)
(NNw : (i : Fin r) → GMod (GΛw i) N)
(w : Fin r → ℤ)
(H : Bar.Cochain Λ (M →ₗ[R] N))
:
ℕ → Bar.Cochain Λ (M →ₗ[R] N)
The successive components.
Instances For
def
MultiplicativeBasisDeformations.GExt.seq0
{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]
{r : ℕ}
{GΛw : Fin r → GAlg Λ}
(MMw : (i : Fin r) → GMod (GΛw i) M)
(NNw : (i : Fin r) → GMod (GΛw i) N)
(w : Fin r → ℤ)
(H : Bar.Cochain Λ (M →ₗ[R] N))
:
ℕ → Bar.Cochain Λ (M →ₗ[R] N)
The successive components of a 0-cochain.
Instances For
theorem
MultiplicativeBasisDeformations.GExt.extVanish_weights1
{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}
{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)
(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))
(hNp : ∀ (i : Fin r) (x p : ℤ) (n : N), NN.gr.IsHom p n → NN.gr.IsHom p (((NNw i).gr.proj x) n))
(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))
(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))
{t : ℤ}
(hExt : ExtVanish MM NN 1 t)
(w : Fin r → ℤ)
(F : Bar.Cochain Λ (M →ₗ[R] N))
(hF : Good MM NN 2 t F)
(hFw : ∀ (i : Fin r), Good (MMw i) (NNw i) 2 (w i) F)
(hdF : (Bar.d (homAct MM NN) 2) F = 0)
:
∃ (H : Bar.Cochain Λ (M →ₗ[R] N)),
Good MM NN 1 t H ∧ (∀ (i : Fin r), Good (MMw i) (NNw i) 1 (w i) H) ∧ (Bar.d (homAct MM NN) 1) H = F
Ext² corrections homogeneous for all the weights at once.
theorem
MultiplicativeBasisDeformations.GExt.extVanish_weights0
{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}
{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))
{t : ℤ}
(hExt : ExtVanish MM NN 0 t)
(w : Fin r → ℤ)
(F : Bar.Cochain Λ (M →ₗ[R] N))
(hF : Good MM NN 1 t F)
(hFw : ∀ (i : Fin r), Good (MMw i) (NNw i) 1 (w i) F)
(hdF : (Bar.d (homAct MM NN) 1) F = 0)
:
∃ (H : Bar.Cochain Λ (M →ₗ[R] N)),
Good MM NN 0 t H ∧ (∀ (i : Fin r), Good (MMw i) (NNw i) 0 (w i) H) ∧ (Bar.d (homAct MM NN) 0) H = F
Ext¹ corrections homogeneous for all the weights at once.