Weight-homogeneous lifts of module actions (toward Proposition 12.8) #
deformation-refinements.tex: the degree-by-degree lifting of Proposition 6.5 with the
choices "made separately in each degree and weight". If the deformation μ_q and the action of
M have all relative weights in a monoid C (ConeBil), the corrections can be taken with
relative weights in C: the error of the next degree has weights in C, and the cone part of
any correction removing it removes it as well, since the correction equation commutes with the
cone parts (cbil). Hence a lifted action with all relative weights in C
(exists_actFam_cone).
structure
MultiplicativeBasisDeformations.GExt.WtCompat
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{M : Type u_3}
[AddCommGroup M]
[Module R M]
(MM : GMod GΛ M)
{Wt : Type u_4}
[AddCommGroup Wt]
[DecidableEq Wt]
(wΛ : MGr R Wt Λ)
(wM : MGr R Wt M)
:
Weight gradings compatible with the product, the action and the internal degrees.
Instances For
theorem
MultiplicativeBasisDeformations.GExt.ConeAt.congr'
{R : Type u_1}
[CommRing R]
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{Wt : Type u_4}
[AddCommGroup Wt]
[DecidableEq Wt]
{C : AddSubmonoid Wt}
{σ σ' : Wt}
{G : MGr R Wt M}
{n : M}
(h : MGr.ConeAt C G σ n)
(e : σ = σ')
:
MGr.ConeAt C G σ' n
theorem
MultiplicativeBasisDeformations.GExt.assocErr_coneAt
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{Wt : Type u_4}
[AddCommGroup Wt]
[DecidableEq Wt]
{C : AddSubmonoid Wt}
{wΛ : MGr R Wt Λ}
{wM : MGr R Wt M}
{ν : ℕ → M →ₗ[R] Λ →ₗ[R] M}
{μ : ℕ → Λ →ₗ[R] Λ →ₗ[R] Λ}
(hν : ∀ (i : ℕ), MGr.ConeBil 0 (ν i))
(hμ : ∀ (j : ℕ), MGr.ConeBil 0 (μ j))
(n : ℕ)
{β α α' : Wt}
{m : M}
{a b : Λ}
(hm : wM.IsHom β m)
(ha : wΛ.IsHom α a)
(hb : wΛ.IsHom α' b)
:
MGr.ConeAt C wM (β + α + α') (assocErr ν μ n m a b)
The error of a family with weights in the cone has weights in the cone.
theorem
MultiplicativeBasisDeformations.GExt.assocErr_eq_zero_of_wt
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{Wt : Type u_4}
[AddCommGroup Wt]
[DecidableEq Wt]
{wΛ : MGr R Wt Λ}
{wM : MGr R Wt M}
(ν : ℕ → M →ₗ[R] Λ →ₗ[R] M)
(μ : ℕ → Λ →ₗ[R] Λ →ₗ[R] Λ)
(n : ℕ)
(h : ∀ (β α α' : Wt) (m : M) (a b : Λ), wM.IsHom β m → wΛ.IsHom α a → wΛ.IsHom α' b → assocErr ν μ n m a b = 0)
(m : M)
(a b : Λ)
:
assocErr ν μ n m a b = 0
A trilinear identity holds when it holds on weight-homogeneous inputs.
theorem
MultiplicativeBasisDeformations.GExt.act_coneBil
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{MM : GMod GΛ M}
{Wt : Type u_4}
[AddCommGroup Wt]
[DecidableEq Wt]
{C : AddSubmonoid Wt}
{wΛ : MGr R Wt Λ}
{wM : MGr R Wt M}
(hW : WtCompat MM wΛ wM)
:
MGr.ConeBil 0 MM.act
theorem
MultiplicativeBasisDeformations.GExt.actFlip_shift
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{MM : GMod GΛ M}
{Wt : Type u_4}
[AddCommGroup Wt]
[DecidableEq Wt]
{wΛ : MGr R Wt Λ}
{wM : MGr R Wt M}
(hW : WtCompat MM wΛ wM)
{α : Wt}
{b : Λ}
(hb : wΛ.IsHom α b)
:
theorem
MultiplicativeBasisDeformations.GExt.cpart_isHom
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{MM : GMod GΛ M}
{Wt : Type u_4}
[AddCommGroup Wt]
[DecidableEq Wt]
{C : AddSubmonoid Wt}
{wΛ : MGr R Wt Λ}
{wM : MGr R Wt M}
(hW : WtCompat MM wΛ wM)
{σ : Wt}
{p : ℤ}
{m : M}
(hm : MM.gr.IsHom p m)
:
The cone part preserves the internal degree.
theorem
MultiplicativeBasisDeformations.GExt.isShift_cbil
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{MM : GMod GΛ M}
{Wt : Type u_4}
[AddCommGroup Wt]
[DecidableEq Wt]
{C : AddSubmonoid Wt}
{wΛ : MGr R Wt Λ}
{wM : MGr R Wt M}
(hW : WtCompat MM wΛ wM)
{n : ℤ}
{D : M →ₗ[R] Λ →ₗ[R] M}
(hD : IsShift MM n D)
:
theorem
MultiplicativeBasisDeformations.GExt.isShift_cbil'
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{MM : GMod GΛ M}
{Wt : Type u_4}
[AddCommGroup Wt]
[DecidableEq Wt]
{C : AddSubmonoid Wt}
{wΛ : MGr R Wt Λ}
{wM : MGr R Wt M}
(hW : WtCompat MM wΛ wM)
(ρ : Wt)
{n : ℤ}
{D : M →ₗ[R] Λ →ₗ[R] M}
(hD : IsShift MM n D)
:
theorem
MultiplicativeBasisDeformations.GExt.corr_cbil
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{MM : GMod GΛ M}
{Wt : Type u_4}
[AddCommGroup Wt]
[DecidableEq Wt]
{C : AddSubmonoid Wt}
{wΛ : MGr R Wt Λ}
{wM : MGr R Wt M}
(hW : WtCompat MM wΛ wM)
(D : M →ₗ[R] Λ →ₗ[R] M)
{β α α' : Wt}
{m : M}
{a b : Λ}
(hm : wM.IsHom β m)
(ha : wΛ.IsHom α a)
(hb : wΛ.IsHom α' b)
:
The correction equation commutes with the cone parts.
theorem
MultiplicativeBasisDeformations.GExt.ConeAt.of_bot
{R : Type u_1}
[CommRing R]
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{Wt : Type u_4}
[AddCommGroup Wt]
[DecidableEq Wt]
{C : AddSubmonoid Wt}
{G : MGr R Wt M}
{σ : Wt}
{n : M}
(h : MGr.ConeAt ⊥ G σ n)
:
MGr.ConeAt C G σ n
theorem
MultiplicativeBasisDeformations.GExt.coneBil_sub
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{Wt : Type u_4}
[AddCommGroup Wt]
[DecidableEq Wt]
{C : AddSubmonoid Wt}
{wΛ : MGr R Wt Λ}
{wM : MGr R Wt M}
{ρ : Wt}
{φ ψ : M →ₗ[R] Λ →ₗ[R] M}
(hφ : MGr.ConeBil ρ φ)
(hψ : MGr.ConeBil ρ ψ)
:
MGr.ConeBil ρ (φ - ψ)
noncomputable def
MultiplicativeBasisDeformations.GExt.corr
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{Wt : Type u_4}
[AddCommGroup Wt]
[DecidableEq Wt]
{C : AddSubmonoid Wt}
{wΛ : MGr R Wt Λ}
{wM : MGr R Wt M}
(D : M →ₗ[R] Λ →ₗ[R] M)
:
M →ₗ[R] Λ →ₗ[R] M
The correction removing the error, with relative weights in the cone minus 0.
Instances For
theorem
MultiplicativeBasisDeformations.GExt.coneBil_corr
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{Wt : Type u_4}
[AddCommGroup Wt]
[DecidableEq Wt]
{C : AddSubmonoid Wt}
{wΛ : MGr R Wt Λ}
{wM : MGr R Wt M}
(D : M →ₗ[R] Λ →ₗ[R] M)
:
MGr.ConeBil 0 (corr D)
theorem
MultiplicativeBasisDeformations.GExt.corr_bottom
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{Wt : Type u_4}
[AddCommGroup Wt]
[DecidableEq Wt]
{C : AddSubmonoid Wt}
{wΛ : MGr R Wt Λ}
{wM : MGr R Wt M}
(D : M →ₗ[R] Λ →ₗ[R] M)
{β α : Wt}
{m : M}
{a : Λ}
(hm : wM.IsHom β m)
(ha : wΛ.IsHom α a)
:
theorem
MultiplicativeBasisDeformations.GExt.isShift_corr
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{MM : GMod GΛ M}
{Wt : Type u_4}
[AddCommGroup Wt]
[DecidableEq Wt]
{C : AddSubmonoid Wt}
{wΛ : MGr R Wt Λ}
{wM : MGr R Wt M}
(hW : WtCompat MM wΛ wM)
{n : ℤ}
{D : M →ₗ[R] Λ →ₗ[R] M}
(hD : IsShift MM n D)
:
theorem
MultiplicativeBasisDeformations.GExt.assocErr_bottom
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{MM : GMod GΛ M}
{Wt : Type u_4}
[AddCommGroup Wt]
[DecidableEq Wt]
{C : AddSubmonoid Wt}
{wΛ : MGr R Wt Λ}
{wM : MGr R Wt M}
(hCp : ∀ γ ∈ C, ∀ δ ∈ C, γ + δ = 0 → γ = 0)
{ν : ℕ → M →ₗ[R] Λ →ₗ[R] M}
{μ : ℕ → Λ →ₗ[R] Λ →ₗ[R] Λ}
(hν : ∀ (i : ℕ), MGr.ConeBil 0 (ν i))
(hμ : ∀ (j : ℕ), MGr.ConeBil 0 (μ j))
(hν0 : ∀ (m : M) (a : Λ), ((ν 0) m) a = (MM.act m) a)
(hμ0 : ∀ (a b : Λ), ((μ 0) a) b = a * b)
(hW : WtCompat MM wΛ wM)
(hνb :
∀ (i : ℕ), 1 ≤ i → ∀ (β α : Wt) (m : M) (a : Λ), wM.IsHom β m → wΛ.IsHom α a → (wM.proj (β + α)) (((ν i) m) a) = 0)
(hμb : ∀ (j : ℕ), 1 ≤ j → ∀ (α α' : Wt) (a b : Λ), wΛ.IsHom α a → wΛ.IsHom α' b → (wΛ.proj (α + α')) (((μ j) a) b) = 0)
{n : ℕ}
(hn : 1 ≤ n)
{β α α' : Wt}
{m : M}
{a b : Λ}
(hm : wM.IsHom β m)
(ha : wΛ.IsHom α a)
(hb : wΛ.IsHom α' b)
:
The error has no bottom component when the lower corrections have none.
theorem
MultiplicativeBasisDeformations.GExt.exists_partial_cone
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{M : Type u_3}
[AddCommGroup M]
[Module R M]
(MM : GMod GΛ M)
{Wt : Type u_4}
[AddCommGroup Wt]
[DecidableEq Wt]
{C : AddSubmonoid Wt}
{wΛ : MGr R Wt Λ}
{wM : MGr R Wt M}
(hW : WtCompat MM wΛ wM)
(hCp : ∀ γ ∈ C, ∀ δ ∈ C, γ + δ = 0 → γ = 0)
(P : PosDef GΛ)
(hP : ∀ (q : ℕ), MGr.ConeBil 0 (P.μ q))
(hPb :
∀ (q : ℕ), 1 ≤ q → ∀ (α α' : Wt) (a b : Λ), wΛ.IsHom α a → wΛ.IsHom α' b → (wΛ.proj (α + α')) (((P.μ q) a) b) = 0)
(hExt : ∀ (t : ℕ), 0 < t → ExtVanish MM MM 1 ↑t)
(N : ℕ)
:
∃ (ν : ℕ → M →ₗ[R] Λ →ₗ[R] M),
(∀ (m : M) (a : Λ), ((ν 0) m) a = (MM.act m) a) ∧ (∀ (n : ℕ), IsShift MM (↑n) (ν n)) ∧ (∀ (n : ℕ), N < n → ν n = 0) ∧ (∀ n ≤ N, ∀ (m : M) (a b : Λ), assocErr ν P.μ n m a b = 0) ∧ (∀ (n : ℕ), MGr.ConeBil 0 (ν n)) ∧ ∀ (n : ℕ),
1 ≤ n → ∀ (β α : Wt) (m : M) (a : Λ), wM.IsHom β m → wΛ.IsHom α a → (wM.proj (β + α)) (((ν n) m) a) = 0
The degree-by-degree construction with homogeneous choices, without corrections of
relative weight 0.
theorem
MultiplicativeBasisDeformations.GExt.exists_actFam_cone
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{M : Type u_3}
[AddCommGroup M]
[Module R M]
(MM : GMod GΛ M)
{Wt : Type u_4}
[AddCommGroup Wt]
[DecidableEq Wt]
{C : AddSubmonoid Wt}
{wΛ : MGr R Wt Λ}
{wM : MGr R Wt M}
(hW : WtCompat MM wΛ wM)
(hCp : ∀ γ ∈ C, ∀ δ ∈ C, γ + δ = 0 → γ = 0)
(P : PosDef GΛ)
(hP : ∀ (q : ℕ), MGr.ConeBil 0 (P.μ q))
(hPb :
∀ (q : ℕ), 1 ≤ q → ∀ (α α' : Wt) (a b : Λ), wΛ.IsHom α a → wΛ.IsHom α' b → (wΛ.proj (α + α')) (((P.μ q) a) b) = 0)
(hnn : ∀ q ∈ GΛ.gr.supp, 0 ≤ q)
(hExt : ∀ (t : ℕ), 0 < t → ExtVanish MM MM 1 ↑t)
:
Proposition 6.5(1) with homogeneous choices: a lifted action whose corrections all have
relative weights in the cone minus 0.
Weight-homogeneous lifts of maps #
theorem
MultiplicativeBasisDeformations.GExt.interErr_coneAt
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{Wt : Type u_4}
[AddCommGroup Wt]
[DecidableEq Wt]
{C : AddSubmonoid Wt}
{wΛ : MGr R Wt Λ}
{wM : MGr R Wt M}
{N : Type u_5}
[AddCommGroup N]
[Module R N]
{wN : MGr R Wt N}
{F : ℕ → M →ₗ[R] N}
{ν : ℕ → M →ₗ[R] Λ →ₗ[R] M}
{ν' : ℕ → N →ₗ[R] Λ →ₗ[R] N}
{ρ : Wt}
(hF : ∀ (i : ℕ), MGr.ConeLin ρ (F i))
(hν : ∀ (i : ℕ), MGr.ConeBil 0 (ν i))
(hν' : ∀ (i : ℕ), MGr.ConeBil 0 (ν' i))
(n : ℕ)
{β α : Wt}
{m : M}
{a : Λ}
(hm : wM.IsHom β m)
(ha : wΛ.IsHom α a)
:
MGr.ConeAt C wN (β + α + ρ) (interErr F ν ν' n m a)
theorem
MultiplicativeBasisDeformations.GExt.interErr_eq_zero_of_wt
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{Wt : Type u_4}
[AddCommGroup Wt]
[DecidableEq Wt]
{wΛ : MGr R Wt Λ}
{wM : MGr R Wt M}
{N : Type u_5}
[AddCommGroup N]
[Module R N]
(F : ℕ → M →ₗ[R] N)
(ν : ℕ → M →ₗ[R] Λ →ₗ[R] M)
(ν' : ℕ → N →ₗ[R] Λ →ₗ[R] N)
(n : ℕ)
(h : ∀ (β α : Wt) (m : M) (a : Λ), wM.IsHom β m → wΛ.IsHom α a → interErr F ν ν' n m a = 0)
(m : M)
(a : Λ)
:
interErr F ν ν' n m a = 0
theorem
MultiplicativeBasisDeformations.GExt.clin_isHom
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{MM : GMod GΛ M}
{Wt : Type u_4}
[AddCommGroup Wt]
[DecidableEq Wt]
{C : AddSubmonoid Wt}
{wΛ : MGr R Wt Λ}
{wM : MGr R Wt M}
(hW : WtCompat MM wΛ wM)
{N : Type u_5}
[AddCommGroup N]
[Module R N]
{NN : GMod GΛ N}
{wN : MGr R Wt N}
(hW' : WtCompat NN wΛ wN)
{ρ : Wt}
{r : ℤ}
{D : M →ₗ[R] N}
(hD : ∀ (p : ℤ) (m : M), MM.gr.IsHom p m → NN.gr.IsHom (p + r) (D m))
(p : ℤ)
(m : M)
:
theorem
MultiplicativeBasisDeformations.GExt.corrMap_clin
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{MM : GMod GΛ M}
{Wt : Type u_4}
[AddCommGroup Wt]
[DecidableEq Wt]
{C : AddSubmonoid Wt}
{wΛ : MGr R Wt Λ}
{wM : MGr R Wt M}
(hW : WtCompat MM wΛ wM)
{N : Type u_5}
[AddCommGroup N]
[Module R N]
{NN : GMod GΛ N}
{wN : MGr R Wt N}
(hW' : WtCompat NN wΛ wN)
(ρ : Wt)
(D : M →ₗ[R] N)
{β α : Wt}
{m : M}
{a : Λ}
(hm : wM.IsHom β m)
(ha : wΛ.IsHom α a)
:
The map correction equation commutes with the cone parts.
theorem
MultiplicativeBasisDeformations.GExt.interErr_bottom
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{MM : GMod GΛ M}
{Wt : Type u_4}
[AddCommGroup Wt]
[DecidableEq Wt]
{C : AddSubmonoid Wt}
{wΛ : MGr R Wt Λ}
{wM : MGr R Wt M}
(hCp : ∀ γ ∈ C, ∀ δ ∈ C, γ + δ = 0 → γ = 0)
{N : Type u_5}
[AddCommGroup N]
[Module R N]
{wN : MGr R Wt N}
{F : ℕ → M →ₗ[R] N}
{ν : ℕ → M →ₗ[R] Λ →ₗ[R] M}
{ν' : ℕ → N →ₗ[R] Λ →ₗ[R] N}
{ρ : Wt}
(hF : ∀ (i : ℕ), MGr.ConeLin ρ (F i))
(hν : ∀ (i : ℕ), MGr.ConeBil 0 (ν i))
(hν' : ∀ (i : ℕ), MGr.ConeBil 0 (ν' i))
(hν0 : ∀ (m : M) (a : Λ), ((ν 0) m) a = (MM.act m) a)
(hW : WtCompat MM wΛ wM)
(hF0 : ∀ (β : Wt) (m : M), wM.IsHom β m → wN.IsHom (β + ρ) ((F 0) m))
(hFb : ∀ (i : ℕ), 1 ≤ i → ∀ (β : Wt) (m : M), wM.IsHom β m → (wN.proj (β + ρ)) ((F i) m) = 0)
(hνb :
∀ (i : ℕ), 1 ≤ i → ∀ (β α : Wt) (m : M) (a : Λ), wM.IsHom β m → wΛ.IsHom α a → (wM.proj (β + α)) (((ν i) m) a) = 0)
(hν'b :
∀ (i : ℕ), 1 ≤ i → ∀ (β α : Wt) (m : N) (a : Λ), wN.IsHom β m → wΛ.IsHom α a → (wN.proj (β + α)) (((ν' i) m) a) = 0)
{n : ℕ}
(hn : 1 ≤ n)
{β α : Wt}
{m : M}
{a : Λ}
(hm : wM.IsHom β m)
(ha : wΛ.IsHom α a)
:
The linearity error has no bottom component when the lower corrections have none.
theorem
MultiplicativeBasisDeformations.GExt.coneLin_of_shift
{R : Type u_1}
[CommRing R]
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{Wt : Type u_4}
[AddCommGroup Wt]
[DecidableEq Wt]
{C : AddSubmonoid Wt}
{wM : MGr R Wt M}
{N : Type u_5}
[AddCommGroup N]
[Module R N]
{wN : MGr R Wt N}
{ρ : Wt}
{g : M →ₗ[R] N}
(hg : ∀ (β : Wt) (m : M), wM.IsHom β m → wN.IsHom (β + ρ) (g m))
:
MGr.ConeLin ρ g
noncomputable def
MultiplicativeBasisDeformations.GExt.corrMap
{R : Type u_1}
[CommRing R]
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{Wt : Type u_4}
[AddCommGroup Wt]
[DecidableEq Wt]
{C : AddSubmonoid Wt}
{wM : MGr R Wt M}
{N : Type u_5}
[AddCommGroup N]
[Module R N]
{wN : MGr R Wt N}
{ρ : Wt}
(D : M →ₗ[R] N)
:
M →ₗ[R] N
The map correction with relative weights in the cone minus 0.
Instances For
theorem
MultiplicativeBasisDeformations.GExt.exists_partialMap_cone
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{MM : GMod GΛ M}
{Wt : Type u_4}
[AddCommGroup Wt]
[DecidableEq Wt]
{C : AddSubmonoid Wt}
{wΛ : MGr R Wt Λ}
{wM : MGr R Wt M}
(hW : WtCompat MM wΛ wM)
(hCp : ∀ γ ∈ C, ∀ δ ∈ C, γ + δ = 0 → γ = 0)
{N : Type u_5}
[AddCommGroup N]
[Module R N]
{NN : GMod GΛ N}
{wN : MGr R Wt N}
(hW' : WtCompat NN wΛ wN)
(P : PosDef GΛ)
(L : ActFam P MM)
(L' : ActFam P NN)
(hL : ∀ (i : ℕ), MGr.ConeBil 0 (L.ν i))
(hL' : ∀ (i : ℕ), MGr.ConeBil 0 (L'.ν i))
(hLb :
∀ (i : ℕ), 1 ≤ i → ∀ (β α : Wt) (m : M) (a : Λ), wM.IsHom β m → wΛ.IsHom α a → (wM.proj (β + α)) (((L.ν i) m) a) = 0)
(hL'b :
∀ (i : ℕ), 1 ≤ i → ∀ (β α : Wt) (m : N) (a : Λ), wN.IsHom β m → wΛ.IsHom α a → (wN.proj (β + α)) (((L'.ν i) m) a) = 0)
{r : ℤ}
{ρ : Wt}
(f : M →ₗ[R] N)
(hf : ∀ (m : M) (a : Λ), f ((MM.act m) a) = (NN.act (f m)) a)
(hfd : ∀ (p : ℤ) (m : M), MM.gr.IsHom p m → NN.gr.IsHom (p + r) (f m))
(hfc : ∀ (β : Wt) (m : M), wM.IsHom β m → wN.IsHom (β + ρ) (f m))
(hExt : ∀ (t : ℕ), 0 < t → ExtVanish MM NN 0 (r + ↑t))
(K : ℕ)
:
∃ (F : ℕ → M →ₗ[R] N),
F 0 = f ∧ (∀ (i : ℕ) (p : ℤ) (m : M), MM.gr.IsHom p m → NN.gr.IsHom (p + r + ↑i) ((F i) m)) ∧ (∀ (n : ℕ), K < n → F n = 0) ∧ (∀ n ≤ K, ∀ (m : M) (a : Λ), interErr F L.ν L'.ν n m a = 0) ∧ (∀ (i : ℕ), MGr.ConeLin ρ (F i)) ∧ ∀ (i : ℕ), 1 ≤ i → ∀ (β : Wt) (m : M), wM.IsHom β m → (wN.proj (β + ρ)) ((F i) m) = 0
The degree-by-degree lift of a map with homogeneous choices, without corrections of
relative weight 0.
theorem
MultiplicativeBasisDeformations.GExt.exists_liftMap_cone
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{MM : GMod GΛ M}
{Wt : Type u_4}
[AddCommGroup Wt]
[DecidableEq Wt]
{C : AddSubmonoid Wt}
{wΛ : MGr R Wt Λ}
{wM : MGr R Wt M}
(hW : WtCompat MM wΛ wM)
(hCp : ∀ γ ∈ C, ∀ δ ∈ C, γ + δ = 0 → γ = 0)
{N : Type u_5}
[AddCommGroup N]
[Module R N]
{NN : GMod GΛ N}
{wN : MGr R Wt N}
(hW' : WtCompat NN wΛ wN)
(P : PosDef GΛ)
(L : ActFam P MM)
(L' : ActFam P NN)
(hL : ∀ (i : ℕ), MGr.ConeBil 0 (L.ν i))
(hL' : ∀ (i : ℕ), MGr.ConeBil 0 (L'.ν i))
(hLb :
∀ (i : ℕ), 1 ≤ i → ∀ (β α : Wt) (m : M) (a : Λ), wM.IsHom β m → wΛ.IsHom α a → (wM.proj (β + α)) (((L.ν i) m) a) = 0)
(hL'b :
∀ (i : ℕ), 1 ≤ i → ∀ (β α : Wt) (m : N) (a : Λ), wN.IsHom β m → wΛ.IsHom α a → (wN.proj (β + α)) (((L'.ν i) m) a) = 0)
{r : ℤ}
{ρ : Wt}
(f : M →ₗ[R] N)
(hf : ∀ (m : M) (a : Λ), f ((MM.act m) a) = (NN.act (f m)) a)
(hfd : ∀ (p : ℤ) (m : M), MM.gr.IsHom p m → NN.gr.IsHom (p + r) (f m))
(hfc : ∀ (β : Wt) (m : M), wM.IsHom β m → wN.IsHom (β + ρ) (f m))
(hnn : ∀ q ∈ GΛ.gr.supp, 0 ≤ q)
(hExt : ∀ (t : ℕ), 0 < t → ExtVanish MM NN 0 (r + ↑t))
:
Proposition 6.5(2) with homogeneous choices.