Gradings of modules by an abelian group #
Used for the integer weights of Section 7 (weights-and-parameters.tex): "a mesh weight w grades V_{m+1}(C) … and grades U_m(C) …; the map D_m
preserves these gradings", and "Lift a basis of the integer ray weights to mesh weights
… These give simultaneous gradings on the lifted modules. If μ has character χ, give
ε weight −χ and choose the homogeneous solutions in the lemma."
A grading MGr of an R-module by an abelian group M is a family of finitely
supported orthogonal projections. A linear map shifts by γ if it sends weight g to
weight g + γ; the weight-γ part of an arbitrary linear map is pr γ φ. Homogeneous
solutions of linear equations are obtained by applying pr to arbitrary solutions,
since pr commutes with composition by shifting maps (pr_comp_left, pr_comp_right).
structure
MultiplicativeBasisDeformations.MGr
(R : Type u_1)
[CommRing R]
(M : Type u_2)
[DecidableEq M]
(N : Type u_3)
[AddCommGroup N]
[Module R N]
:
Type (max u_2 u_3)
A grading by M, by finitely supported orthogonal projections.
- proj : M → N →ₗ[R] N
- supp : Finset M
Instances For
theorem
MultiplicativeBasisDeformations.MGr.ext_of_hom
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[DecidableEq M]
{N : Type u_3}
[AddCommGroup N]
[Module R N]
(G : MGr R M N)
{P : Type u_6}
[AddCommGroup P]
[Module R P]
{f f' : N →ₗ[R] P}
(h : ∀ (g : M) (n : N), G.IsHom g n → f n = f' n)
:
f = f'
Linear maps agreeing on homogeneous elements agree.
theorem
MultiplicativeBasisDeformations.MGr.eq_of_proj
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[DecidableEq M]
{N : Type u_3}
[AddCommGroup N]
[Module R N]
(G : MGr R M N)
{n n' : N}
(h : ∀ (g : M), (G.proj g) n = (G.proj g) n')
:
n = n'
Elements with the same components are equal.
theorem
MultiplicativeBasisDeformations.MGr.proj_sum_hom
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[DecidableEq M]
{N : Type u_3}
[AddCommGroup N]
[Module R N]
(G : MGr R M N)
{ι : Type u_6}
(s : Finset ι)
(f : ι → N)
(w : ι → M)
(hf : ∀ i ∈ s, G.IsHom (w i) (f i))
(g : M)
:
(G.proj g) (∑ i ∈ s, f i) = ∑ i ∈ s with w i = g, f i
The projection of a homogeneous sum.
Shifting maps #
def
MultiplicativeBasisDeformations.MGr.Shift
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[DecidableEq M]
{N : Type u_3}
{N' : Type u_4}
[AddCommGroup N]
[Module R N]
[AddCommGroup N']
[Module R N']
(G : MGr R M N)
(G' : MGr R M N')
(γ : M)
(φ : N →ₗ[R] N')
:
φ shifts weights by γ.
Instances For
theorem
MultiplicativeBasisDeformations.MGr.Shift.add
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[DecidableEq M]
{N : Type u_3}
{N' : Type u_4}
[AddCommGroup N]
[Module R N]
[AddCommGroup N']
[Module R N']
{G : MGr R M N}
{G' : MGr R M N'}
{γ : M}
{φ ψ : N →ₗ[R] N'}
(hφ : G.Shift G' γ φ)
(hψ : G.Shift G' γ ψ)
:
G.Shift G' γ (φ + ψ)
theorem
MultiplicativeBasisDeformations.MGr.Shift.sub
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[DecidableEq M]
{N : Type u_3}
{N' : Type u_4}
[AddCommGroup N]
[Module R N]
[AddCommGroup N']
[Module R N']
{G : MGr R M N}
{G' : MGr R M N'}
{γ : M}
{φ ψ : N →ₗ[R] N'}
(hφ : G.Shift G' γ φ)
(hψ : G.Shift G' γ ψ)
:
G.Shift G' γ (φ - ψ)
theorem
MultiplicativeBasisDeformations.MGr.Shift.smul
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[DecidableEq M]
{N : Type u_3}
{N' : Type u_4}
[AddCommGroup N]
[Module R N]
[AddCommGroup N']
[Module R N']
{G : MGr R M N}
{G' : MGr R M N'}
{γ : M}
{φ : N →ₗ[R] N'}
(hφ : G.Shift G' γ φ)
(c : R)
:
G.Shift G' γ (c • φ)
theorem
MultiplicativeBasisDeformations.MGr.Shift.sum
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[DecidableEq M]
{N : Type u_3}
{N' : Type u_4}
[AddCommGroup N]
[Module R N]
[AddCommGroup N']
[Module R N']
{G : MGr R M N}
{G' : MGr R M N'}
{γ : M}
{ι : Type u_6}
(s : Finset ι)
{φ : ι → N →ₗ[R] N'}
(h : ∀ i ∈ s, G.Shift G' γ (φ i))
:
G.Shift G' γ (∑ i ∈ s, φ i)
theorem
MultiplicativeBasisDeformations.MGr.Shift.comp
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[DecidableEq M]
{N : Type u_3}
{N' : Type u_4}
{N'' : Type u_5}
[AddCommGroup N]
[Module R N]
[AddCommGroup N']
[Module R N']
[AddCommGroup N'']
[Module R N'']
{G : MGr R M N}
{G' : MGr R M N'}
{G'' : MGr R M N''}
{γ δ : M}
{φ : N →ₗ[R] N'}
{ψ : N' →ₗ[R] N''}
(hψ : G'.Shift G'' δ ψ)
(hφ : G.Shift G' γ φ)
:
G.Shift G'' (γ + δ) (ψ ∘ₗ φ)
theorem
MultiplicativeBasisDeformations.MGr.Shift.congr
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[DecidableEq M]
{N : Type u_3}
{N' : Type u_4}
[AddCommGroup N]
[Module R N]
[AddCommGroup N']
[Module R N']
{G : MGr R M N}
{G' : MGr R M N'}
{γ γ' : M}
{φ : N →ₗ[R] N'}
(hφ : G.Shift G' γ φ)
(h : γ = γ')
:
G.Shift G' γ' φ
theorem
MultiplicativeBasisDeformations.MGr.Shift.proj
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[DecidableEq M]
{N : Type u_3}
{N' : Type u_4}
[AddCommGroup N]
[Module R N]
[AddCommGroup N']
[Module R N']
{G : MGr R M N}
{G' : MGr R M N'}
{γ : M}
{φ : N →ₗ[R] N'}
(hφ : G.Shift G' γ φ)
(g : M)
(n : N)
:
A shifting map commutes with the projections.
def
MultiplicativeBasisDeformations.MGr.pr
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[DecidableEq M]
{N : Type u_3}
{N' : Type u_4}
[AddCommGroup N]
[Module R N]
[AddCommGroup N']
[Module R N']
(G : MGr R M N)
(G' : MGr R M N')
(γ : M)
(φ : N →ₗ[R] N')
:
N →ₗ[R] N'
The weight-γ part of a linear map.
Instances For
theorem
MultiplicativeBasisDeformations.MGr.pr_apply_hom
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[DecidableEq M]
{N : Type u_3}
{N' : Type u_4}
[AddCommGroup N]
[Module R N]
[AddCommGroup N']
[Module R N']
{G : MGr R M N}
{G' : MGr R M N'}
(γ : M)
(φ : N →ₗ[R] N')
{g : M}
{n : N}
(hn : G.IsHom g n)
:
theorem
MultiplicativeBasisDeformations.MGr.pr_of_shift
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[DecidableEq M]
{N : Type u_3}
{N' : Type u_4}
[AddCommGroup N]
[Module R N]
[AddCommGroup N']
[Module R N']
{G : MGr R M N}
{G' : MGr R M N'}
{γ : M}
{φ : N →ₗ[R] N'}
(hφ : G.Shift G' γ φ)
:
G.pr G' γ φ = φ
theorem
MultiplicativeBasisDeformations.MGr.pr_sum
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[DecidableEq M]
{N : Type u_3}
{N' : Type u_4}
[AddCommGroup N]
[Module R N]
[AddCommGroup N']
[Module R N']
{G : MGr R M N}
{G' : MGr R M N'}
(γ : M)
{ι : Type u_6}
(s : Finset ι)
(φ : ι → N →ₗ[R] N')
:
theorem
MultiplicativeBasisDeformations.MGr.pr_comp_left
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[DecidableEq M]
{N : Type u_3}
{N' : Type u_4}
{N'' : Type u_5}
[AddCommGroup N]
[Module R N]
[AddCommGroup N']
[Module R N']
[AddCommGroup N'']
[Module R N'']
{G : MGr R M N}
{G' : MGr R M N'}
{G'' : MGr R M N''}
{γ δ : M}
(φ : N →ₗ[R] N')
{ψ : N' →ₗ[R] N''}
(hψ : G'.Shift G'' δ ψ)
:
Composition on the left with a shifting map.
theorem
MultiplicativeBasisDeformations.MGr.pr_comp_right
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[DecidableEq M]
{N : Type u_3}
{N' : Type u_4}
{N'' : Type u_5}
[AddCommGroup N]
[Module R N]
[AddCommGroup N']
[Module R N']
[AddCommGroup N'']
[Module R N'']
{G : MGr R M N}
{G' : MGr R M N'}
{G'' : MGr R M N''}
{γ δ : M}
(φ : N →ₗ[R] N')
{ψ : N'' →ₗ[R] N}
(hψ : G''.Shift G δ ψ)
:
Composition on the right with a shifting map.