Weights in a cone (toward Proposition 12.8) #
deformation-refinements.tex: "For each bar differential choose a k-linear right
inverse on its image; […] Make these choices separately in each degree and weight". In the family
m + Σ_i t_i μ_i the parameter t_i carries the weight χ_i of μ_i, so the lifts are
homogeneous when every component has relative weight in the monoid C spanned by the χ_i.
For a weight grading G and σ, ConeAt C σ n says that the components of n have weights in
σ + C, and cpart C σ projects onto them. Maps shifting weights by γ move σ + C to
σ + γ + C (ConeAt.shift); maps and bilinear maps whose components have relative weights in C
(ConeLin, ConeBil) preserve the cone condition, and their cone parts are clin, cbil.
theorem
MultiplicativeBasisDeformations.MGr.proj_cpart
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[DecidableEq M]
{C : AddSubmonoid M}
{N : Type u_3}
[AddCommGroup N]
[Module R N]
{G : MGr R M N}
(σ δ : M)
(n : N)
:
theorem
MultiplicativeBasisDeformations.MGr.ConeAt.sum
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[DecidableEq M]
{C : AddSubmonoid M}
{N : Type u_3}
[AddCommGroup N]
[Module R N]
{G : MGr R M N}
{σ : M}
{ι : Type u_6}
(s : Finset ι)
{n : ι → N}
(h : ∀ i ∈ s, ConeAt C G σ (n i))
:
ConeAt C G σ (∑ i ∈ s, n i)
theorem
MultiplicativeBasisDeformations.MGr.ConeAt.shift
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[DecidableEq M]
{C : AddSubmonoid 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' γ φ)
{n : N}
(h : ConeAt C G σ n)
:
ConeAt C G' (σ + γ) (φ n)
Shifting maps move the cone.
theorem
MultiplicativeBasisDeformations.MGr.cpart_shift
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[DecidableEq M]
{C : AddSubmonoid 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' γ φ)
(n : N)
:
Shifting maps commute with the cone parts.
Maps with relative weights in the cone #
def
MultiplicativeBasisDeformations.MGr.ConeLin
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[DecidableEq M]
{C : AddSubmonoid 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)
(f : N →ₗ[R] N')
:
The components of f have relative weights in ρ + C.
Instances For
def
MultiplicativeBasisDeformations.MGr.ConeBil
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[DecidableEq M]
{C : AddSubmonoid 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' →ₗ[R] N'')
:
The components of φ have relative weights in ρ + C.
Instances For
theorem
MultiplicativeBasisDeformations.MGr.ConeLin.apply
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[DecidableEq M]
{C : AddSubmonoid 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}
{f : N →ₗ[R] N'}
(hf : ConeLin ρ f)
{n : N}
(hn : ConeAt C G σ n)
:
ConeAt C G' (σ + ρ) (f n)
A cone condition on the input propagates.
theorem
MultiplicativeBasisDeformations.MGr.ConeBil.apply
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[DecidableEq M]
{C : AddSubmonoid 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' →ₗ[R] N''}
(hφ : ConeBil ρ φ)
{n : N}
{n' : N'}
(hn : ConeAt C G σ n)
(hn' : ConeAt C G' σ' n')
:
ConeAt C G'' (σ + σ' + ρ) ((φ n) n')
noncomputable def
MultiplicativeBasisDeformations.MGr.clin
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[DecidableEq M]
(C : AddSubmonoid 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)
(f : N →ₗ[R] N')
:
N →ₗ[R] N'
The cone part of a linear map relative to ρ.
Instances For
theorem
MultiplicativeBasisDeformations.MGr.clin_apply_hom
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[DecidableEq M]
{C : AddSubmonoid 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)
(f : N →ₗ[R] N')
{β : M}
{n : N}
(hn : G.IsHom β n)
:
theorem
MultiplicativeBasisDeformations.MGr.coneLin_clin
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[DecidableEq M]
{C : AddSubmonoid 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)
(f : N →ₗ[R] N')
:
theorem
MultiplicativeBasisDeformations.MGr.clin_of_coneLin
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[DecidableEq M]
{C : AddSubmonoid 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}
{f : N →ₗ[R] N'}
(hf : ConeLin ρ f)
:
clin C G G' ρ f = f
noncomputable def
MultiplicativeBasisDeformations.MGr.cbil
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[DecidableEq M]
(C : AddSubmonoid 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' →ₗ[R] N'')
:
N →ₗ[R] N' →ₗ[R] N''
The cone part of a bilinear map relative to ρ.
Instances For
theorem
MultiplicativeBasisDeformations.MGr.cbil_apply_hom
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[DecidableEq M]
{C : AddSubmonoid 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' →ₗ[R] N'')
{β α : M}
{n : N}
{n' : N'}
(hn : G.IsHom β n)
(hn' : G'.IsHom α n')
:
theorem
MultiplicativeBasisDeformations.MGr.coneBil_cbil
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[DecidableEq M]
{C : AddSubmonoid 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' →ₗ[R] N'')
:
theorem
MultiplicativeBasisDeformations.MGr.bil_ext_of_hom
{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'}
{φ ψ : N →ₗ[R] N' →ₗ[R] N''}
(h : ∀ (β α : M) (n : N) (n' : N'), G.IsHom β n → G'.IsHom α n' → (φ n) n' = (ψ n) n')
:
φ = ψ
Bilinear maps agreeing on homogeneous elements agree.
theorem
MultiplicativeBasisDeformations.MGr.cbil_of_coneBil
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[DecidableEq M]
{C : AddSubmonoid 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' →ₗ[R] N''}
(hφ : ConeBil ρ φ)
:
cbil C G G' G'' ρ φ = φ
Bottom components in a pointed cone #
theorem
MultiplicativeBasisDeformations.MGr.proj_eq_zero_of_coneAt
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[DecidableEq M]
{C : AddSubmonoid M}
{N : Type u_3}
[AddCommGroup N]
[Module R N]
{G : MGr R M N}
(hCp : ∀ γ ∈ C, ∀ δ ∈ C, γ + δ = 0 → γ = 0)
{σ σ' : M}
{n : N}
(h : ConeAt C G σ' n)
(hσ : σ' - σ ∈ C)
(hne : σ' ≠ σ)
:
(G.proj σ) n = 0
theorem
MultiplicativeBasisDeformations.MGr.ConeLin.proj_bottom
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[DecidableEq M]
{C : AddSubmonoid 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'}
(hCp : ∀ γ ∈ C, ∀ δ ∈ C, γ + δ = 0 → γ = 0)
{ρ σ : M}
{f : N →ₗ[R] N'}
(hf : ConeLin ρ f)
{n : N}
(hn : ConeAt C G σ n)
:
Only the bottom component of the input reaches the bottom component of the output.
theorem
MultiplicativeBasisDeformations.MGr.ConeBil.proj_bottom
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[DecidableEq M]
{C : AddSubmonoid 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''}
(hCp : ∀ γ ∈ C, ∀ δ ∈ C, γ + δ = 0 → γ = 0)
{ρ σ σ' : M}
{φ : N →ₗ[R] N' →ₗ[R] N''}
(hφ : ConeBil ρ φ)
{n : N}
{n' : N'}
(hn : ConeAt C G σ n)
(hn' : ConeAt C G' σ' n')
:
theorem
MultiplicativeBasisDeformations.MGr.ConeBil.proj_bottom.ConeAt.congr''
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[DecidableEq M]
{C : AddSubmonoid M}
{N'' : Type u_5}
[AddCommGroup N'']
[Module R N'']
{G'' : MGr R M N''}
{σ₁ σ₂ : M}
{x : N''}
(h : ConeAt C G'' σ₁ x)
(e : σ₁ = σ₂)
:
ConeAt C G'' σ₂ x
Cone conditions on maps: closure properties and bottom parts #
theorem
MultiplicativeBasisDeformations.MGr.ConeLin.zero
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[DecidableEq M]
{C : AddSubmonoid 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)
:
ConeLin ρ 0
theorem
MultiplicativeBasisDeformations.MGr.ConeLin.add
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[DecidableEq M]
{C : AddSubmonoid 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}
{f g : N →ₗ[R] N'}
(hf : ConeLin ρ f)
(hg : ConeLin ρ g)
:
ConeLin ρ (f + g)
theorem
MultiplicativeBasisDeformations.MGr.ConeLin.sub
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[DecidableEq M]
{C : AddSubmonoid 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}
{f g : N →ₗ[R] N'}
(hf : ConeLin ρ f)
(hg : ConeLin ρ g)
:
ConeLin ρ (f - g)
theorem
MultiplicativeBasisDeformations.MGr.ConeLin.smul
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[DecidableEq M]
{C : AddSubmonoid 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}
(c : R)
{f : N →ₗ[R] N'}
(hf : ConeLin ρ f)
:
ConeLin ρ (c • f)
theorem
MultiplicativeBasisDeformations.MGr.ConeLin.sum
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[DecidableEq M]
{C : AddSubmonoid 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 ι)
{f : ι → N →ₗ[R] N'}
(hf : ∀ i ∈ s, ConeLin ρ (f i))
:
ConeLin ρ (∑ i ∈ s, f i)
theorem
MultiplicativeBasisDeformations.MGr.ConeLin.mono
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[DecidableEq M]
{C : AddSubmonoid 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}
{f : N →ₗ[R] N'}
(hf : ConeLin (ρ + γ) f)
(hγ : γ ∈ C)
:
ConeLin ρ f
theorem
MultiplicativeBasisDeformations.MGr.ConeLin.of_shift
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[DecidableEq M]
{C : AddSubmonoid 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}
{f : N →ₗ[R] N'}
(hf : G.Shift G' ρ f)
:
ConeLin ρ f
theorem
MultiplicativeBasisDeformations.MGr.ConeLin.comp
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[DecidableEq M]
{C : AddSubmonoid 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}
{f : N →ₗ[R] N'}
{g : N' →ₗ[R] N''}
(hf : ConeLin ρ f)
(hg : ConeLin ρ' g)
:
ConeLin (ρ + ρ') (g ∘ₗ f)
theorem
MultiplicativeBasisDeformations.MGr.clin_bot_apply
{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)
(f : N →ₗ[R] N')
{β : M}
{n : N}
(hn : G.IsHom β n)
:
theorem
MultiplicativeBasisDeformations.MGr.clin_bot_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 ι)
(f : ι → N →ₗ[R] N')
:
theorem
MultiplicativeBasisDeformations.MGr.clin_bot_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}
{f : N →ₗ[R] N'}
(hf : G.Shift G' ρ f)
:
clin ⊥ G G' ρ f = f
theorem
MultiplicativeBasisDeformations.MGr.clin_bot_of_pos
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[DecidableEq M]
{C : AddSubmonoid 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'}
(hCp : ∀ γ ∈ C, ∀ δ ∈ C, γ + δ = 0 → γ = 0)
{ρ γ : M}
{f : N →ₗ[R] N'}
(hf : ConeLin (ρ + γ) f)
(hγ : γ ∈ C)
(hγ0 : γ ≠ 0)
:
clin ⊥ G G' ρ f = 0
A map whose relative weights lie in γ + C with γ ≠ 0 has no bottom part.
theorem
MultiplicativeBasisDeformations.MGr.clin_bot_comp
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[DecidableEq M]
{C : AddSubmonoid 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''}
(hCp : ∀ γ ∈ C, ∀ δ ∈ C, γ + δ = 0 → γ = 0)
{ρ ρ' : M}
{f : N →ₗ[R] N'}
{g : N' →ₗ[R] N''}
(hf : ConeLin ρ f)
(hg : ConeLin ρ' g)
:
The bottom part of a composite is the composite of the bottom parts.
Components at an atom of the cone #
theorem
MultiplicativeBasisDeformations.MGr.ConeLin.proj_atom
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[DecidableEq M]
{C : AddSubmonoid 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'}
(hCp : ∀ γ ∈ C, ∀ δ ∈ C, γ + δ = 0 → γ = 0)
{γ : M}
(hγ : γ ∈ C)
(hγ0 : γ ≠ 0)
(hat : ∀ u ∈ C, ∀ v ∈ C, u + v = γ → u = 0 ∨ v = 0)
{ρ σ : M}
{f : N →ₗ[R] N'}
(hf : ConeLin ρ f)
{n : N}
(hn : ConeAt C G σ n)
:
Atom components of a linear image: only the bottom and the atom component of the input contribute to the atom component of the output.
theorem
MultiplicativeBasisDeformations.MGr.ConeBil.proj_atom
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[DecidableEq M]
{C : AddSubmonoid 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''}
(hCp : ∀ γ ∈ C, ∀ δ ∈ C, γ + δ = 0 → γ = 0)
{γ : M}
(hγ : γ ∈ C)
(hγ0 : γ ≠ 0)
(hat : ∀ u ∈ C, ∀ v ∈ C, u + v = γ → u = 0 ∨ v = 0)
{ρ σ σ' : M}
{φ : N →ₗ[R] N' →ₗ[R] N''}
(hφ : ConeBil ρ φ)
{n : N}
{n' : N'}
(hn : ConeAt C G σ n)
(hn' : ConeAt C G' σ' n')
:
Atom components of a bilinear image.