Graded modules and graded Ext via the bar complex #
Section 6 (positive-deformations.tex): "Internal degree t in
Hom or Ext means maps from a graded projective resolution to the target which
raise degree by t", computed by the bar resolution. Here graded Ext^n_t(M, N)
is the cohomology of the bar complex Hom_R(M ⊗ Λ^{⊗n}, N) in internal degree
t (Good, ExtVanish), for graded right modules over a graded R-algebra
Λ (R a commutative ring: a field, or ℤ/4 in Section 10).
The bar complex is taken over R rather than relative to S; both compute Ext
(weights-and-parameters.tex for the relative form). That it computes the manuscript's
Ext is proved in ExtResolutions.lean: for every graded projective resolution, the Ext
computed from it vanishes exactly when the bar Ext does (GRes.extVanish_iff).
structure
MultiplicativeBasisDeformations.GExt.ZGr
{R : Type u_1}
[CommRing R]
(M : Type u_2)
[AddCommGroup M]
[Module R M]
:
Type u_2
A ℤ-grading of an R-module by finitely supported projections.
- proj : ℤ → M →ₗ[R] M
- supp : Finset ℤ
Instances For
theorem
MultiplicativeBasisDeformations.GExt.ZGr.ext_of_hom
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
(g : ZGr M)
{N : Type u_3}
[AddCommGroup N]
[Module R N]
{f f' : M →ₗ[R] N}
(h : ∀ (p : ℤ) (m : M), g.IsHom p m → f m = f' m)
:
f = f'
Linear maps that agree on homogeneous elements agree.
def
MultiplicativeBasisDeformations.GExt.homAct
{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)
:
Bar.Act Λ (M →ₗ[R] N)
The bimodule Hom_R(M, N): (a·φ)(m) = φ(ma), (φ·b)(m) = φ(m)b.
Instances For
structure
MultiplicativeBasisDeformations.GExt.Good
{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)
(n : ℕ)
(t : ℤ)
(F : Bar.Cochain Λ (M →ₗ[R] N))
:
Good cochains: the bar cochains M × Λⁿ → N, R-multilinear, of internal
degree t.
- tr (a : ℕ → Λ) : F a = F (Bar.tr n a)
- add (a : ℕ → Λ) (i : ℕ) (x y : Λ) : i < n → F (Function.update a i (x + y)) = F (Function.update a i x) + F (Function.update a i y)
- smul (a : ℕ → Λ) (i : ℕ) (c : R) (x : Λ) : i < n → F (Function.update a i (c • x)) = c • F (Function.update a i x)
Instances For
theorem
MultiplicativeBasisDeformations.GExt.Good.add'
{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}
{n : ℕ}
{t : ℤ}
{F G : Bar.Cochain Λ (M →ₗ[R] N)}
(hF : Good MM NN n t F)
(hG : Good MM NN n t G)
:
Good MM NN n t (F + G)
theorem
MultiplicativeBasisDeformations.GExt.Good.zsmul'
{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}
{n : ℕ}
{t : ℤ}
{F : Bar.Cochain Λ (M →ₗ[R] N)}
(hF : Good MM NN n t F)
(z : ℤ)
:
Good MM NN n t (z • F)
theorem
MultiplicativeBasisDeformations.GExt.Good.sum'
{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}
{n : ℕ}
{t : ℤ}
{ι : Type u_5}
(s : Finset ι)
{F : ι → Bar.Cochain Λ (M →ₗ[R] N)}
(h : ∀ i ∈ s, Good MM NN n t (F i))
:
Good MM NN n t (∑ i ∈ s, F i)
theorem
MultiplicativeBasisDeformations.GExt.sum_range_contract
(n p : ℕ)
(hp : p < n)
(ds : ℕ → ℤ)
:
(∑ k ∈ Finset.range n, if k < p then ds k else if k = p then ds p + ds (p + 1) else ds (k + 1)) = ∑ k ∈ Finset.range (n + 1), ds k
theorem
MultiplicativeBasisDeformations.GExt.Good.coface
{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}
{n : ℕ}
{t : ℤ}
{F : Bar.Cochain Λ (M →ₗ[R] N)}
(hF : Good MM NN n t F)
(j : ℕ)
(hj : j ≤ n + 1)
:
Good MM NN (n + 1) t ((Bar.coface (homAct MM NN) n j) F)
Cofaces preserve good cochains.
theorem
MultiplicativeBasisDeformations.GExt.Good.d
{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}
{n : ℕ}
{t : ℤ}
{F : Bar.Cochain Λ (M →ₗ[R] N)}
(hF : Good MM NN n t F)
:
d preserves good cochains.
def
MultiplicativeBasisDeformations.GExt.ExtVanish
{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)
(n : ℕ)
(t : ℤ)
:
Ext^{n+1}_t(M, N) = 0: every good cocycle is a good coboundary.
Instances For
Pullback along module maps #
def
MultiplicativeBasisDeformations.GExt.pull
{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]
{M' : Type u_5}
[AddCommGroup M']
[Module R M']
(π : M' →ₗ[R] M)
(F : Bar.Cochain Λ (M →ₗ[R] N))
:
Bar.Cochain Λ (M' →ₗ[R] N)
Pullback of cochains along π : M' → M.
Instances For
theorem
MultiplicativeBasisDeformations.GExt.pull_apply
{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]
{M' : Type u_5}
[AddCommGroup M']
[Module R M']
(π : M' →ₗ[R] M)
(F : Bar.Cochain Λ (M →ₗ[R] N))
(a : ℕ → Λ)
(m : M')
:
(pull π F a) m = (F a) (π m)
theorem
MultiplicativeBasisDeformations.GExt.pull_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]
{M' : Type u_5}
[AddCommGroup M']
[Module R M']
(π : M' →ₗ[R] M)
(F G : Bar.Cochain Λ (M →ₗ[R] N))
:
theorem
MultiplicativeBasisDeformations.GExt.pull_sub
{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]
{M' : Type u_5}
[AddCommGroup M']
[Module R M']
(π : M' →ₗ[R] M)
(F G : Bar.Cochain Λ (M →ₗ[R] N))
:
theorem
MultiplicativeBasisDeformations.GExt.pull_comp
{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]
{M' : Type u_5}
[AddCommGroup M']
[Module R M']
{M'' : Type u_6}
[AddCommGroup M'']
[Module R M'']
(π : M' →ₗ[R] M)
(π' : M'' →ₗ[R] M')
(F : Bar.Cochain Λ (M →ₗ[R] N))
:
theorem
MultiplicativeBasisDeformations.GExt.pull_id
{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]
(F : Bar.Cochain Λ (M →ₗ[R] N))
:
pull LinearMap.id F = F
theorem
MultiplicativeBasisDeformations.GExt.coface_pull
{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}
{M' : Type u_5}
[AddCommGroup M']
[Module R M']
{MM' : GMod GΛ M'}
{π : M' →ₗ[R] M}
(hπ : ∀ (m : M') (a : Λ), π ((MM'.act m) a) = (MM.act (π m)) a)
(n j : ℕ)
(F : Bar.Cochain Λ (M →ₗ[R] N))
:
(Bar.coface (homAct MM' NN) n j) (pull π F) = pull π ((Bar.coface (homAct MM NN) n j) F)
Pullback along a Λ-linear map commutes with the cofaces.
theorem
MultiplicativeBasisDeformations.GExt.d_pull
{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}
{M' : Type u_5}
[AddCommGroup M']
[Module R M']
{MM' : GMod GΛ M'}
{π : M' →ₗ[R] M}
(hπ : ∀ (m : M') (a : Λ), π ((MM'.act m) a) = (MM.act (π m)) a)
(n : ℕ)
(F : Bar.Cochain Λ (M →ₗ[R] N))
:
Pullback along a Λ-linear map commutes with d.
theorem
MultiplicativeBasisDeformations.GExt.Good.pull
{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}
{M' : Type u_5}
[AddCommGroup M']
[Module R M']
{MM' : GMod GΛ M'}
{n : ℕ}
{t s : ℤ}
{F : Bar.Cochain Λ (M →ₗ[R] N)}
(hF : Good MM NN n t F)
{π : M' →ₗ[R] M}
(hπ : ∀ (p : ℤ) (m : M'), MM'.gr.IsHom p m → MM.gr.IsHom (p + s) (π m))
:
Pullback along a map of degree s sends good cochains of degree t to good
cochains of degree t + s.
Cyclic projective modules #
structure
MultiplicativeBasisDeformations.GExt.CycProj
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{P : Type u_6}
[AddCommGroup P]
[Module R P]
(PP : GMod GΛ P)
:
Type (max u_2 u_6)
A cyclic graded projective P ≅ eΛ⟨b⟩ with generator g.
- e : Λ
- g : P
- b : ℤ
- ψ : P →ₗ[R] Λ
Instances For
theorem
MultiplicativeBasisDeformations.GExt.CycProj.extVanish
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{N : Type u_4}
[AddCommGroup N]
[Module R N]
{P : Type u_6}
[AddCommGroup P]
[Module R P]
{PP : GMod GΛ P}
(C : CycProj PP)
(NN : GMod GΛ N)
(n : ℕ)
(t : ℤ)
:
ExtVanish PP NN n t
Ext^{n+1} out of a cyclic projective vanishes, by the contracting
homotopy H(a)(m) = F(ψ m, a)(g).
theorem
MultiplicativeBasisDeformations.GExt.pull_map_sub
{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]
{M' : Type u_5}
[AddCommGroup M']
[Module R M']
(f g : M' →ₗ[R] M)
(F : Bar.Cochain Λ (M →ₗ[R] N))
:
theorem
MultiplicativeBasisDeformations.GExt.pull_map_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]
{M' : Type u_5}
[AddCommGroup M']
[Module R M']
(f g : M' →ₗ[R] M)
(F : Bar.Cochain Λ (M →ₗ[R] N))
:
theorem
MultiplicativeBasisDeformations.GExt.pull_zero_map
{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]
{M' : Type u_5}
[AddCommGroup M']
[Module R M']
(F : Bar.Cochain Λ (M →ₗ[R] N))
:
pull 0 F = 0
theorem
MultiplicativeBasisDeformations.GExt.pull_d_sub
{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]
{M' : Type u_5}
[AddCommGroup M']
[Module R M']
(π : M' →ₗ[R] M)
(A : Bar.Act Λ (M →ₗ[R] N))
(n : ℕ)
(F G : Bar.Cochain Λ (M →ₗ[R] N))
:
theorem
MultiplicativeBasisDeformations.GExt.extVanish_of_decomp
{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}
{ι : Type u_7}
[Fintype ι]
{Ms : ι → Type u_8}
[(a : ι) → AddCommGroup (Ms a)]
[(a : ι) → Module R (Ms a)]
(MMs : (a : ι) → GMod GΛ (Ms a))
(s : ι → ℤ)
(inc : (a : ι) → Ms a →ₗ[R] M)
(pr : (a : ι) → M →ₗ[R] Ms a)
(hinc : ∀ (a : ι) (m : Ms a) (x : Λ), (inc a) (((MMs a).act m) x) = (MM.act ((inc a) m)) x)
(hpr : ∀ (a : ι) (m : M) (x : Λ), (pr a) ((MM.act m) x) = ((MMs a).act ((pr a) m)) x)
(hinc_deg : ∀ (a : ι) (p : ℤ) (m : Ms a), (MMs a).gr.IsHom p m → MM.gr.IsHom (p + s a) ((inc a) m))
(hpr_deg : ∀ (a : ι) (p : ℤ) (m : M), MM.gr.IsHom p m → (MMs a).gr.IsHom (p + -s a) ((pr a) m))
(hsum : ∀ (m : M), ∑ a : ι, (inc a) ((pr a) m) = m)
(n : ℕ)
(t : ℤ)
(h : ∀ (a : ι), inc a ≠ 0 → ExtVanish (MMs a) NN n (t + s a))
:
ExtVanish MM NN n t
Additivity: Ext vanishing passes to a finite graded direct sum
M = ⊕ M_a⟨s_a⟩.
theorem
MultiplicativeBasisDeformations.GExt.extVanish_shift
{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}
{K : Type u_7}
{P : Type u_8}
[AddCommGroup K]
[Module R K]
[AddCommGroup P]
[Module R P]
{KK : GMod GΛ K}
{PP : GMod GΛ P}
(ι : K →ₗ[R] P)
(π : P →ₗ[R] M)
(s : M →ₗ[R] P)
(ρ : P →ₗ[R] K)
(hι : ∀ (m : K) (a : Λ), ι ((KK.act m) a) = (PP.act (ι m)) a)
(hπ : ∀ (m : P) (a : Λ), π ((PP.act m) a) = (MM.act (π m)) a)
(hι_deg : ∀ (p : ℤ) (m : K), KK.gr.IsHom p m → PP.gr.IsHom (p + 0) (ι m))
(hπ_deg : ∀ (p : ℤ) (m : P), PP.gr.IsHom p m → MM.gr.IsHom (p + 0) (π m))
(hs_deg : ∀ (p : ℤ) (m : M), MM.gr.IsHom p m → PP.gr.IsHom (p + 0) (s m))
(hρ_deg : ∀ (p : ℤ) (m : P), PP.gr.IsHom p m → KK.gr.IsHom (p + 0) (ρ m))
(hπs : π ∘ₗ s = LinearMap.id)
(hρι : ρ ∘ₗ ι = LinearMap.id)
(hsplit : ι ∘ₗ ρ + s ∘ₗ π = LinearMap.id)
(hπι : π ∘ₗ ι = 0)
{n : ℕ}
{t : ℤ}
(hP : ExtVanish PP NN (n + 1) t)
(hK : ExtVanish KK NN n t)
:
ExtVanish MM NN (n + 1) t
Dimension shifting: for an R-split exact sequence 0 → K → P → M → 0 of
graded modules with Ext^{n+2}(P, -)_t = 0, Ext^{n+1}(K, N)_t = 0 gives
Ext^{n+2}(M, N)_t = 0.
Ext¹ and graded extensions #
The sequence (a, 0, 0, …).
Instances For
theorem
MultiplicativeBasisDeformations.GExt.Good.one_eq
{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}
{t : ℤ}
{F : Bar.Cochain Λ (M →ₗ[R] N)}
(hF : Good MM NN 1 t F)
(a : ℕ → Λ)
:
F a = F (single (a 0))
theorem
MultiplicativeBasisDeformations.GExt.cocycle_one
{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}
{F : Bar.Cochain Λ (M →ₗ[R] N)}
{t : ℤ}
(hF : Good MM NN 1 t F)
(hd : (Bar.d (homAct MM NN) 1) F = 0)
(a b : Λ)
(m : M)
:
The cocycle equation of a one-cochain.
theorem
MultiplicativeBasisDeformations.GExt.Good.single_add
{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}
{t : ℤ}
{F : Bar.Cochain Λ (M →ₗ[R] N)}
(hF : Good MM NN 1 t F)
(a a' : Λ)
:
theorem
MultiplicativeBasisDeformations.GExt.Good.single_smul
{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}
{t : ℤ}
{F : Bar.Cochain Λ (M →ₗ[R] N)}
(hF : Good MM NN 1 t F)
(c : R)
(a : Λ)
:
def
MultiplicativeBasisDeformations.GExt.twistGr
{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}
(t : ℤ)
:
ZGr (N × M)
The grading of N⟨-t⟩ ⊕ M.
Instances For
def
MultiplicativeBasisDeformations.GExt.twist
{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}
{t : ℤ}
(F : Bar.Cochain Λ (M →ₗ[R] N))
(hF : Good MM NN 1 t F)
(hd : (Bar.d (homAct MM NN) 1) F = 0)
:
GMod GΛ (N × M)
The extension defined by a one-cocycle: N⟨-t⟩ ⊕ M with
(n, m)·a = (na + F(a)(m), ma).
Instances For
theorem
MultiplicativeBasisDeformations.GExt.coboundary_of_section
{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}
{t : ℤ}
{F : Bar.Cochain Λ (M →ₗ[R] N)}
(hF : Good MM NN 1 t F)
(hd : (Bar.d (homAct MM NN) 1) F = 0)
(σ : M →ₗ[R] N × M)
(hσ2 : ∀ (m : M), (σ m).2 = m)
(hσ : ∀ (m : M) (a : Λ), σ ((MM.act m) a) = ((twist F hF hd).act (σ m)) a)
(hσdeg : ∀ (p : ℤ) (m : M), MM.gr.IsHom p m → (twistGr t).IsHom p (σ m))
:
∃ (φ : Bar.Cochain Λ (M →ₗ[R] N)), Good MM NN 0 t φ ∧ (Bar.d (homAct MM NN) 0) φ = F
A graded section of the extension makes the cocycle a coboundary.
Homogeneous components of module maps #
theorem
MultiplicativeBasisDeformations.GExt.lsum_comp
{R : Type u_1}
[CommRing R]
{X : Type u_7}
{Y : Type u_8}
{Z : Type u_9}
[AddCommGroup X]
[Module R X]
[AddCommGroup Y]
[Module R Y]
[AddCommGroup Z]
[Module R Z]
{ι : Type u_10}
(S : Finset ι)
(f : ι → Y →ₗ[R] Z)
(g : X →ₗ[R] Y)
:
(∑ i ∈ S, f i) ∘ₗ g = ∑ i ∈ S, f i ∘ₗ g
theorem
MultiplicativeBasisDeformations.GExt.lcomp_sum
{R : Type u_1}
[CommRing R]
{X : Type u_7}
{Y : Type u_8}
{Z : Type u_9}
[AddCommGroup X]
[Module R X]
[AddCommGroup Y]
[Module R Y]
[AddCommGroup Z]
[Module R Z]
{ι : Type u_10}
(S : Finset ι)
(g : Y →ₗ[R] Z)
(f : ι → X →ₗ[R] Y)
:
g ∘ₗ ∑ i ∈ S, f i = ∑ i ∈ S, g ∘ₗ f i
def
MultiplicativeBasisDeformations.GExt.ZGr.comp
{R : Type u_1}
[CommRing R]
{X : Type u_7}
{Y : Type u_8}
[AddCommGroup X]
[Module R X]
[AddCommGroup Y]
[Module R Y]
(gX : ZGr X)
(gY : ZGr Y)
(r : ℤ)
(u : X →ₗ[R] Y)
:
X →ₗ[R] Y
The degree-r component Σ_p proj_{p+r} ∘ u ∘ proj_p of a linear map.
Instances For
theorem
MultiplicativeBasisDeformations.GExt.ZGr.comp_eq_zero_of_hom
{R : Type u_1}
[CommRing R]
{X : Type u_7}
{Y : Type u_8}
[AddCommGroup X]
[Module R X]
[AddCommGroup Y]
[Module R Y]
(gX : ZGr X)
(gY : ZGr Y)
{r : ℤ}
{u : X →ₗ[R] Y}
{s : ℤ}
(hu : ∀ (p : ℤ) (m : X), gX.IsHom p m → gY.IsHom (p + s) (u m))
(hrs : r ≠ s)
:
gX.comp gY r u = 0
theorem
MultiplicativeBasisDeformations.GExt.ZGr.comp_eq_self_of_hom
{R : Type u_1}
[CommRing R]
{X : Type u_7}
{Y : Type u_8}
[AddCommGroup X]
[Module R X]
[AddCommGroup Y]
[Module R Y]
(gX : ZGr X)
(gY : ZGr Y)
{s : ℤ}
{u : X →ₗ[R] Y}
(hu : ∀ (p : ℤ) (m : X), gX.IsHom p m → gY.IsHom (p + s) (u m))
:
gX.comp gY s u = u
theorem
MultiplicativeBasisDeformations.GExt.ZGr.comp_comp_left
{R : Type u_1}
[CommRing R]
{X : Type u_7}
{Y : Type u_8}
[AddCommGroup X]
[Module R X]
[AddCommGroup Y]
[Module R Y]
(gX : ZGr X)
(gY : ZGr Y)
{Z : Type u_9}
[AddCommGroup Z]
[Module R Z]
(gZ : ZGr Z)
(r : ℤ)
(u : X →ₗ[R] Y)
(v : Y →ₗ[R] Z)
(hv : ∀ (p : ℤ) (m : Y), gY.IsHom p m → gZ.IsHom p (v m))
:
theorem
MultiplicativeBasisDeformations.GExt.ZGr.comp_comp_right
{R : Type u_1}
[CommRing R]
{X : Type u_7}
{Y : Type u_8}
[AddCommGroup X]
[Module R X]
[AddCommGroup Y]
[Module R Y]
(gX : ZGr X)
(gY : ZGr Y)
{W : Type u_9}
[AddCommGroup W]
[Module R W]
(gW : ZGr W)
(r : ℤ)
(u : X →ₗ[R] Y)
(w : W →ₗ[R] X)
(hw : ∀ (p : ℤ) (m : W), gW.IsHom p m → gX.IsHom p (w m))
:
theorem
MultiplicativeBasisDeformations.GExt.ZGr.proj_map
{R : Type u_1}
[CommRing R]
{X : Type u_7}
{Y : Type u_8}
[AddCommGroup X]
[Module R X]
[AddCommGroup Y]
[Module R Y]
(gX : ZGr X)
(gY : ZGr Y)
{s : ℤ}
{u : X →ₗ[R] Y}
(hu : ∀ (p : ℤ) (m : X), gX.IsHom p m → gY.IsHom (p + s) (u m))
(p : ℤ)
(m : X)
:
A homogeneous map of degree s commutes with the projections.
theorem
MultiplicativeBasisDeformations.GExt.ZGr.isHom_of_injective
{R : Type u_1}
[CommRing R]
{X : Type u_7}
{Y : Type u_8}
[AddCommGroup X]
[Module R X]
[AddCommGroup Y]
[Module R Y]
(gX : ZGr X)
(gY : ZGr Y)
{s : ℤ}
{u : X →ₗ[R] Y}
(hu : ∀ (p : ℤ) (m : X), gX.IsHom p m → gY.IsHom (p + s) (u m))
(hinj : Function.Injective ⇑u)
{p : ℤ}
{m : X}
(hm : gY.IsHom (p + s) (u m))
:
gX.IsHom p m
An injective homogeneous map reflects homogeneity.
theorem
MultiplicativeBasisDeformations.GExt.ZGr.comp_zero_comp
{R : Type u_1}
[CommRing R]
{X : Type u_7}
{Y : Type u_8}
[AddCommGroup X]
[Module R X]
[AddCommGroup Y]
[Module R Y]
(gX : ZGr X)
(gY : ZGr Y)
{Z : Type u_9}
[AddCommGroup Z]
[Module R Z]
(gZ : ZGr Z)
(u : X →ₗ[R] Y)
(v : Y →ₗ[R] Z)
:
The degree-zero part of a composite is the sum of the matching components.
theorem
MultiplicativeBasisDeformations.GExt.proj_act
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{Y : Type u_8}
[AddCommGroup Y]
[Module R Y]
(YY : GMod GΛ Y)
{q : ℤ}
{a : Λ}
(ha : GΛ.gr.IsHom q a)
(p : ℤ)
(y : Y)
:
Homogeneous components of graded modules commute with the action.
theorem
MultiplicativeBasisDeformations.GExt.comp_act
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{X : Type u_7}
{Y : Type u_8}
[AddCommGroup X]
[Module R X]
[AddCommGroup Y]
[Module R Y]
{XX : GMod GΛ X}
{YY : GMod GΛ Y}
(r : ℤ)
{u : X →ₗ[R] Y}
(hu : ∀ (m : X) (a : Λ), u ((XX.act m) a) = (YY.act (u m)) a)
(m : X)
(a : Λ)
:
Components of Λ-linear maps are Λ-linear.
Finite products with a shift #
def
MultiplicativeBasisDeformations.GExt.ZGr.piShift
{R : Type u_1}
[CommRing R]
{ι : Type u_7}
[Fintype ι]
{Ms : ι → Type u_8}
[(a : ι) → AddCommGroup (Ms a)]
[(a : ι) → Module R (Ms a)]
(gs : (a : ι) → ZGr (Ms a))
(s : ι → ℤ)
:
ZGr ((a : ι) → Ms a)
The grading of ⊕_a M_a⟨s_a⟩: (⊕ M_a)_p = ⊕ (M_a)_{p-s_a}.
Instances For
theorem
MultiplicativeBasisDeformations.GExt.ZGr.piShift_isHom
{R : Type u_1}
[CommRing R]
{ι : Type u_7}
[Fintype ι]
[DecidableEq ι]
{Ms : ι → Type u_8}
[(a : ι) → AddCommGroup (Ms a)]
[(a : ι) → Module R (Ms a)]
(gs : (a : ι) → ZGr (Ms a))
(s : ι → ℤ)
(p : ℤ)
(x : (a : ι) → Ms a)
:
def
MultiplicativeBasisDeformations.GExt.GMod.pi
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{ι : Type u_7}
[Fintype ι]
[DecidableEq ι]
{Ms : ι → Type u_8}
[(a : ι) → AddCommGroup (Ms a)]
[(a : ι) → Module R (Ms a)]
(MMs : (a : ι) → GMod GΛ (Ms a))
(s : ι → ℤ)
:
GMod GΛ ((a : ι) → Ms a)
⊕_a M_a⟨s_a⟩ as a graded module.
Instances For
theorem
MultiplicativeBasisDeformations.GExt.GMod.pi_act
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{ι : Type u_7}
[Fintype ι]
[DecidableEq ι]
{Ms : ι → Type u_8}
[(a : ι) → AddCommGroup (Ms a)]
[(a : ι) → Module R (Ms a)]
(MMs : (a : ι) → GMod GΛ (Ms a))
(s : ι → ℤ)
(x : (a : ι) → Ms a)
(b : Λ)
(a : ι)
:
theorem
MultiplicativeBasisDeformations.GExt.extVanish_pi
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{N : Type u_4}
[AddCommGroup N]
[Module R N]
{NN : GMod GΛ N}
{ι : Type u_7}
[Fintype ι]
[DecidableEq ι]
{Ms : ι → Type u_8}
[(a : ι) → AddCommGroup (Ms a)]
[(a : ι) → Module R (Ms a)]
(MMs : (a : ι) → GMod GΛ (Ms a))
(s : ι → ℤ)
(n : ℕ)
(t : ℤ)
(h : ∀ (a : ι), ExtVanish (MMs a) NN n (t + s a))
:
Ext out of a finite sum of shifts.
Left modules over the opposite #
def
MultiplicativeBasisDeformations.GExt.Left
{R : Type u_1}
[CommRing R]
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{B : Type u_7}
[Ring B]
[Algebra R B]
{GB : GAlg Bᵐᵒᵖ}
(_MM : GMod GB M)
:
Type u_3
The underlying left B-module of a graded right Bᵐᵒᵖ… i.e. right B-module
over Λ = Bᵐᵒᵖ: b • m = m·(op b).
Instances For
def
MultiplicativeBasisDeformations.GExt.Left.map
{R : Type u_1}
[CommRing R]
{M : Type u_3}
{N : Type u_4}
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{B : Type u_7}
[Ring B]
[Algebra R B]
{GB : GAlg Bᵐᵒᵖ}
(MM : GMod GB M)
{NN : GMod GB N}
(u : M →ₗ[R] N)
(hu : ∀ (m : M) (a : Bᵐᵒᵖ), u ((MM.act m) a) = (NN.act (u m)) a)
:
A Λ-linear map between graded modules as a B-linear map of the left modules.
Instances For
Kernels of graded maps #
theorem
MultiplicativeBasisDeformations.GExt.ker_proj_mem
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{P : Type u_7}
[AddCommGroup P]
[Module R P]
(PP : GMod GΛ P)
(MM : GMod GΛ M)
{π : P →ₗ[R] M}
(hdeg : ∀ (p : ℤ) (x : P), PP.gr.IsHom p x → MM.gr.IsHom (p + 0) (π x))
(p : ℤ)
{x : P}
(hx : x ∈ π.ker)
:
def
MultiplicativeBasisDeformations.GExt.ZGr.ker
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{P : Type u_7}
[AddCommGroup P]
[Module R P]
(PP : GMod GΛ P)
(MM : GMod GΛ M)
{π : P →ₗ[R] M}
(hdeg : ∀ (p : ℤ) (x : P), PP.gr.IsHom p x → MM.gr.IsHom (p + 0) (π x))
:
ZGr ↥π.ker
The grading of a kernel.
Instances For
theorem
MultiplicativeBasisDeformations.GExt.ZGr.ker_isHom
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{P : Type u_7}
[AddCommGroup P]
[Module R P]
(PP : GMod GΛ P)
(MM : GMod GΛ M)
{π : P →ₗ[R] M}
(hdeg : ∀ (p : ℤ) (x : P), PP.gr.IsHom p x → MM.gr.IsHom (p + 0) (π x))
(p : ℤ)
(x : ↥π.ker)
:
theorem
MultiplicativeBasisDeformations.GExt.ker_act_mem
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{P : Type u_7}
[AddCommGroup P]
[Module R P]
(PP : GMod GΛ P)
(MM : GMod GΛ M)
{π : P →ₗ[R] M}
(hπ : ∀ (x : P) (a : Λ), π ((PP.act x) a) = (MM.act (π x)) a)
(x : ↥π.ker)
(a : Λ)
:
(PP.act ↑x) a ∈ π.ker
def
MultiplicativeBasisDeformations.GExt.GMod.ker
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{P : Type u_7}
[AddCommGroup P]
[Module R P]
(PP : GMod GΛ P)
(MM : GMod GΛ M)
{π : P →ₗ[R] M}
(hπ : ∀ (x : P) (a : Λ), π ((PP.act x) a) = (MM.act (π x)) a)
(hdeg : ∀ (p : ℤ) (x : P), PP.gr.IsHom p x → MM.gr.IsHom (p + 0) (π x))
:
GMod GΛ ↥π.ker
The kernel of a graded map as a graded module.
Instances For
theorem
MultiplicativeBasisDeformations.GExt.GMod.ker_act
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{P : Type u_7}
[AddCommGroup P]
[Module R P]
(PP : GMod GΛ P)
(MM : GMod GΛ M)
{π : P →ₗ[R] M}
(hπ : ∀ (x : P) (a : Λ), π ((PP.act x) a) = (MM.act (π x)) a)
(hdeg : ∀ (p : ℤ) (x : P), PP.gr.IsHom p x → MM.gr.IsHom (p + 0) (π x))
(x : ↥π.ker)
(a : Λ)
: