Lifting graded modules and maps to ℤ/4 (Proposition 10.1, the lifting steps) #
integral-deformations.tex (proof of prop:fixed-integral-companion): "Lift the action
matrices arbitrarily to free graded 𝒪-modules. Their associativity defect is even. Division
by two, followed by reduction, gives an Ext² class of degree zero. Equation
(prime-field-ext-vanishing) supplies a correction. Since (2𝒪)² = 0, this single correction
makes the action associative. The same bar calculation, using Ext¹, gives uniqueness and
lifts all homogeneous maps of nonnegative degree."
Setting: a graded 𝔽₂-algebra Λ, a graded 𝒪-algebra Λ̃ (𝒪 = ℤ/4) and a reduction
π : Λ̃ → Λ. A lift of a graded Λ-module M is a graded Λ̃-module M̃ with a reduction
ρ : M̃ → M whose kernel is 2M̃ and the annihilator of two (IsLift). Twice a lift
(tw) and division by two (half) are well defined; maps of degree d lift when
Ext¹_d vanishes (exists_liftHom).
structure
MultiplicativeBasisDeformations.WLift.IsRed
{Λ : Type u_1}
[Ring Λ]
[Algebra (ZMod 2) Λ]
{Λ' : Type u_2}
[Ring Λ']
[Algebra (ZMod 4) Λ']
(GΛ' : GExt.GAlg Λ')
(GΛ : GExt.GAlg Λ)
(π : Λ' →+* Λ)
:
A reduction of graded algebras Λ̃ → Λ along ℤ/4 → 𝔽₂.
- ker (x : Λ') : π x = 0 → ∃ (y : Λ'), x = 2 • y
- ann (x : Λ') : 2 • x = 0 → π x = 0
Instances For
structure
MultiplicativeBasisDeformations.WLift.IsLift
{Λ : Type u_1}
[Ring Λ]
[Algebra (ZMod 2) Λ]
{GΛ : GExt.GAlg Λ}
{Λ' : Type u_2}
[Ring Λ']
[Algebra (ZMod 4) Λ']
{GΛ' : GExt.GAlg Λ'}
{M : Type u_3}
[AddCommGroup M]
[Module (ZMod 2) M]
{M' : Type u_4}
[AddCommGroup M']
[Module (ZMod 4) M']
(MM' : GExt.GMod GΛ' M')
(MM : GExt.GMod GΛ M)
(π : Λ' →+* Λ)
(ρ : M' →+ M)
:
A lift of a graded module.
- ker (m : M') : ρ m = 0 → ∃ (m' : M'), m = 2 • m'
- ann (m : M') : 2 • m = 0 → ρ m = 0
Instances For
theorem
MultiplicativeBasisDeformations.WLift.IsLift.ρ_surj
{Λ : Type u_1}
[Ring Λ]
[Algebra (ZMod 2) Λ]
{GΛ : GExt.GAlg Λ}
{Λ' : Type u_2}
[Ring Λ']
[Algebra (ZMod 4) Λ']
{GΛ' : GExt.GAlg Λ'}
{π : Λ' →+* Λ}
{M : Type u_3}
[AddCommGroup M]
[Module (ZMod 2) M]
{M' : Type u_4}
[AddCommGroup M']
[Module (ZMod 4) M']
{MM' : GExt.GMod GΛ' M'}
{MM : GExt.GMod GΛ M}
{ρ : M' →+ M}
(H : IsLift MM' MM π ρ)
(m : M)
:
∃ (m' : M'), ρ m' = m
theorem
MultiplicativeBasisDeformations.WLift.IsLift.two_smul_eq_of_ρ
{Λ : Type u_1}
[Ring Λ]
[Algebra (ZMod 2) Λ]
{GΛ : GExt.GAlg Λ}
{Λ' : Type u_2}
[Ring Λ']
[Algebra (ZMod 4) Λ']
{GΛ' : GExt.GAlg Λ'}
{π : Λ' →+* Λ}
{M : Type u_3}
[AddCommGroup M]
[Module (ZMod 2) M]
{M' : Type u_4}
[AddCommGroup M']
[Module (ZMod 4) M']
{MM' : GExt.GMod GΛ' M'}
{MM : GExt.GMod GΛ M}
{ρ : M' →+ M}
(H : IsLift MM' MM π ρ)
{m n : M'}
(h : ρ m = ρ n)
:
2 • m = 2 • n
theorem
MultiplicativeBasisDeformations.WLift.IsLift.ρ_two_smul
{Λ : Type u_1}
[Ring Λ]
[Algebra (ZMod 2) Λ]
{GΛ : GExt.GAlg Λ}
{Λ' : Type u_2}
[Ring Λ']
[Algebra (ZMod 4) Λ']
{GΛ' : GExt.GAlg Λ'}
{π : Λ' →+* Λ}
{M : Type u_3}
[AddCommGroup M]
[Module (ZMod 2) M]
{M' : Type u_4}
[AddCommGroup M']
[Module (ZMod 4) M']
{MM' : GExt.GMod GΛ' M'}
{MM : GExt.GMod GΛ M}
{ρ : M' →+ M}
(H : IsLift MM' MM π ρ)
(m : M')
:
ρ (2 • m) = 0
theorem
MultiplicativeBasisDeformations.WLift.IsLift.two_smul_two_smul
{Λ : Type u_1}
[Ring Λ]
[Algebra (ZMod 2) Λ]
{GΛ : GExt.GAlg Λ}
{Λ' : Type u_2}
[Ring Λ']
[Algebra (ZMod 4) Λ']
{GΛ' : GExt.GAlg Λ'}
{π : Λ' →+* Λ}
{M : Type u_3}
[AddCommGroup M]
[Module (ZMod 2) M]
{M' : Type u_4}
[AddCommGroup M']
[Module (ZMod 4) M']
{MM' : GExt.GMod GΛ' M'}
{MM : GExt.GMod GΛ M}
{ρ : M' →+ M}
(H : IsLift MM' MM π ρ)
(m : M')
:
2 • 2 • m = 0
noncomputable def
MultiplicativeBasisDeformations.WLift.IsLift.tw
{Λ : Type u_1}
[Ring Λ]
[Algebra (ZMod 2) Λ]
{GΛ : GExt.GAlg Λ}
{Λ' : Type u_2}
[Ring Λ']
[Algebra (ZMod 4) Λ']
{GΛ' : GExt.GAlg Λ'}
{π : Λ' →+* Λ}
{M : Type u_3}
[AddCommGroup M]
[Module (ZMod 2) M]
{M' : Type u_4}
[AddCommGroup M']
[Module (ZMod 4) M']
{MM' : GExt.GMod GΛ' M'}
{MM : GExt.GMod GΛ M}
{ρ : M' →+ M}
(H : IsLift MM' MM π ρ)
:
M →+ M'
Twice a lift, M → 2M̃.
Instances For
theorem
MultiplicativeBasisDeformations.WLift.IsLift.tw_ρ
{Λ : Type u_1}
[Ring Λ]
[Algebra (ZMod 2) Λ]
{GΛ : GExt.GAlg Λ}
{Λ' : Type u_2}
[Ring Λ']
[Algebra (ZMod 4) Λ']
{GΛ' : GExt.GAlg Λ'}
{π : Λ' →+* Λ}
{M : Type u_3}
[AddCommGroup M]
[Module (ZMod 2) M]
{M' : Type u_4}
[AddCommGroup M']
[Module (ZMod 4) M']
{MM' : GExt.GMod GΛ' M'}
{MM : GExt.GMod GΛ M}
{ρ : M' →+ M}
(H : IsLift MM' MM π ρ)
(m : M')
:
H.tw (ρ m) = 2 • m
theorem
MultiplicativeBasisDeformations.WLift.IsLift.tw_smul
{Λ : Type u_1}
[Ring Λ]
[Algebra (ZMod 2) Λ]
{GΛ : GExt.GAlg Λ}
{Λ' : Type u_2}
[Ring Λ']
[Algebra (ZMod 4) Λ']
{GΛ' : GExt.GAlg Λ'}
{π : Λ' →+* Λ}
{M : Type u_3}
[AddCommGroup M]
[Module (ZMod 2) M]
{M' : Type u_4}
[AddCommGroup M']
[Module (ZMod 4) M']
{MM' : GExt.GMod GΛ' M'}
{MM : GExt.GMod GΛ M}
{ρ : M' →+ M}
(H : IsLift MM' MM π ρ)
(a : ZMod 4)
(m : M)
:
theorem
MultiplicativeBasisDeformations.WLift.IsLift.tw_smul_k
{Λ : Type u_1}
[Ring Λ]
[Algebra (ZMod 2) Λ]
{GΛ : GExt.GAlg Λ}
{Λ' : Type u_2}
[Ring Λ']
[Algebra (ZMod 4) Λ']
{GΛ' : GExt.GAlg Λ'}
{π : Λ' →+* Λ}
{M : Type u_3}
[AddCommGroup M]
[Module (ZMod 2) M]
{M' : Type u_4}
[AddCommGroup M']
[Module (ZMod 4) M']
{MM' : GExt.GMod GΛ' M'}
{MM : GExt.GMod GΛ M}
{ρ : M' →+ M}
(H : IsLift MM' MM π ρ)
(a : ZMod 2)
(m : M)
:
theorem
MultiplicativeBasisDeformations.WLift.IsLift.ρ_tw
{Λ : Type u_1}
[Ring Λ]
[Algebra (ZMod 2) Λ]
{GΛ : GExt.GAlg Λ}
{Λ' : Type u_2}
[Ring Λ']
[Algebra (ZMod 4) Λ']
{GΛ' : GExt.GAlg Λ'}
{π : Λ' →+* Λ}
{M : Type u_3}
[AddCommGroup M]
[Module (ZMod 2) M]
{M' : Type u_4}
[AddCommGroup M']
[Module (ZMod 4) M']
{MM' : GExt.GMod GΛ' M'}
{MM : GExt.GMod GΛ M}
{ρ : M' →+ M}
(H : IsLift MM' MM π ρ)
(m : M)
:
ρ (H.tw m) = 0
theorem
MultiplicativeBasisDeformations.WLift.IsLift.two_smul_tw
{Λ : Type u_1}
[Ring Λ]
[Algebra (ZMod 2) Λ]
{GΛ : GExt.GAlg Λ}
{Λ' : Type u_2}
[Ring Λ']
[Algebra (ZMod 4) Λ']
{GΛ' : GExt.GAlg Λ'}
{π : Λ' →+* Λ}
{M : Type u_3}
[AddCommGroup M]
[Module (ZMod 2) M]
{M' : Type u_4}
[AddCommGroup M']
[Module (ZMod 4) M']
{MM' : GExt.GMod GΛ' M'}
{MM : GExt.GMod GΛ M}
{ρ : M' →+ M}
(H : IsLift MM' MM π ρ)
(m : M)
:
2 • H.tw m = 0
theorem
MultiplicativeBasisDeformations.WLift.IsLift.tw_eq_zero_iff
{Λ : Type u_1}
[Ring Λ]
[Algebra (ZMod 2) Λ]
{GΛ : GExt.GAlg Λ}
{Λ' : Type u_2}
[Ring Λ']
[Algebra (ZMod 4) Λ']
{GΛ' : GExt.GAlg Λ'}
{π : Λ' →+* Λ}
{M : Type u_3}
[AddCommGroup M]
[Module (ZMod 2) M]
{M' : Type u_4}
[AddCommGroup M']
[Module (ZMod 4) M']
{MM' : GExt.GMod GΛ' M'}
{MM : GExt.GMod GΛ M}
{ρ : M' →+ M}
(H : IsLift MM' MM π ρ)
(m : M)
:
H.tw m = 0 ↔ m = 0
theorem
MultiplicativeBasisDeformations.WLift.IsLift.tw_injective
{Λ : Type u_1}
[Ring Λ]
[Algebra (ZMod 2) Λ]
{GΛ : GExt.GAlg Λ}
{Λ' : Type u_2}
[Ring Λ']
[Algebra (ZMod 4) Λ']
{GΛ' : GExt.GAlg Λ'}
{π : Λ' →+* Λ}
{M : Type u_3}
[AddCommGroup M]
[Module (ZMod 2) M]
{M' : Type u_4}
[AddCommGroup M']
[Module (ZMod 4) M']
{MM' : GExt.GMod GΛ' M'}
{MM : GExt.GMod GΛ M}
{ρ : M' →+ M}
(H : IsLift MM' MM π ρ)
:
Function.Injective ⇑H.tw
theorem
MultiplicativeBasisDeformations.WLift.IsLift.tw_act
{Λ : Type u_1}
[Ring Λ]
[Algebra (ZMod 2) Λ]
{GΛ : GExt.GAlg Λ}
{Λ' : Type u_2}
[Ring Λ']
[Algebra (ZMod 4) Λ']
{GΛ' : GExt.GAlg Λ'}
{π : Λ' →+* Λ}
{M : Type u_3}
[AddCommGroup M]
[Module (ZMod 2) M]
{M' : Type u_4}
[AddCommGroup M']
[Module (ZMod 4) M']
{MM' : GExt.GMod GΛ' M'}
{MM : GExt.GMod GΛ M}
{ρ : M' →+ M}
(H : IsLift MM' MM π ρ)
(m : M)
(b : Λ')
:
theorem
MultiplicativeBasisDeformations.WLift.IsLift.tw_deg
{Λ : Type u_1}
[Ring Λ]
[Algebra (ZMod 2) Λ]
{GΛ : GExt.GAlg Λ}
{Λ' : Type u_2}
[Ring Λ']
[Algebra (ZMod 4) Λ']
{GΛ' : GExt.GAlg Λ'}
{π : Λ' →+* Λ}
{M : Type u_3}
[AddCommGroup M]
[Module (ZMod 2) M]
{M' : Type u_4}
[AddCommGroup M']
[Module (ZMod 4) M']
{MM' : GExt.GMod GΛ' M'}
{MM : GExt.GMod GΛ M}
{ρ : M' →+ M}
(H : IsLift MM' MM π ρ)
{p : ℤ}
{m : M}
(hm : MM.gr.IsHom p m)
:
noncomputable def
MultiplicativeBasisDeformations.WLift.IsLift.half
{Λ : Type u_1}
[Ring Λ]
[Algebra (ZMod 2) Λ]
{GΛ : GExt.GAlg Λ}
{Λ' : Type u_2}
[Ring Λ']
[Algebra (ZMod 4) Λ']
{GΛ' : GExt.GAlg Λ'}
{π : Λ' →+* Λ}
{M : Type u_3}
[AddCommGroup M]
[Module (ZMod 2) M]
{M' : Type u_4}
[AddCommGroup M']
[Module (ZMod 4) M']
{MM' : GExt.GMod GΛ' M'}
{MM : GExt.GMod GΛ M}
{ρ : M' →+ M}
(H : IsLift MM' MM π ρ)
(m : M')
:
M
Division by two on the kernel of the reduction: half m with tw (half m) = m.
Instances For
theorem
MultiplicativeBasisDeformations.WLift.IsLift.tw_half
{Λ : Type u_1}
[Ring Λ]
[Algebra (ZMod 2) Λ]
{GΛ : GExt.GAlg Λ}
{Λ' : Type u_2}
[Ring Λ']
[Algebra (ZMod 4) Λ']
{GΛ' : GExt.GAlg Λ'}
{π : Λ' →+* Λ}
{M : Type u_3}
[AddCommGroup M]
[Module (ZMod 2) M]
{M' : Type u_4}
[AddCommGroup M']
[Module (ZMod 4) M']
{MM' : GExt.GMod GΛ' M'}
{MM : GExt.GMod GΛ M}
{ρ : M' →+ M}
(H : IsLift MM' MM π ρ)
{m : M'}
(h : ρ m = 0)
:
theorem
MultiplicativeBasisDeformations.WLift.IsLift.half_eq_of_tw
{Λ : Type u_1}
[Ring Λ]
[Algebra (ZMod 2) Λ]
{GΛ : GExt.GAlg Λ}
{Λ' : Type u_2}
[Ring Λ']
[Algebra (ZMod 4) Λ']
{GΛ' : GExt.GAlg Λ'}
{π : Λ' →+* Λ}
{M : Type u_3}
[AddCommGroup M]
[Module (ZMod 2) M]
{M' : Type u_4}
[AddCommGroup M']
[Module (ZMod 4) M']
{MM' : GExt.GMod GΛ' M'}
{MM : GExt.GMod GΛ M}
{ρ : M' →+ M}
(H : IsLift MM' MM π ρ)
{m : M'}
{n : M}
(h : H.tw n = m)
:
H.half m = n
theorem
MultiplicativeBasisDeformations.WLift.IsLift.half_add
{Λ : Type u_1}
[Ring Λ]
[Algebra (ZMod 2) Λ]
{GΛ : GExt.GAlg Λ}
{Λ' : Type u_2}
[Ring Λ']
[Algebra (ZMod 4) Λ']
{GΛ' : GExt.GAlg Λ'}
{π : Λ' →+* Λ}
{M : Type u_3}
[AddCommGroup M]
[Module (ZMod 2) M]
{M' : Type u_4}
[AddCommGroup M']
[Module (ZMod 4) M']
{MM' : GExt.GMod GΛ' M'}
{MM : GExt.GMod GΛ M}
{ρ : M' →+ M}
(H : IsLift MM' MM π ρ)
{m n : M'}
(hm : ρ m = 0)
(hn : ρ n = 0)
:
theorem
MultiplicativeBasisDeformations.WLift.IsLift.half_sub
{Λ : Type u_1}
[Ring Λ]
[Algebra (ZMod 2) Λ]
{GΛ : GExt.GAlg Λ}
{Λ' : Type u_2}
[Ring Λ']
[Algebra (ZMod 4) Λ']
{GΛ' : GExt.GAlg Λ'}
{π : Λ' →+* Λ}
{M : Type u_3}
[AddCommGroup M]
[Module (ZMod 2) M]
{M' : Type u_4}
[AddCommGroup M']
[Module (ZMod 4) M']
{MM' : GExt.GMod GΛ' M'}
{MM : GExt.GMod GΛ M}
{ρ : M' →+ M}
(H : IsLift MM' MM π ρ)
{m n : M'}
(hm : ρ m = 0)
(hn : ρ n = 0)
:
theorem
MultiplicativeBasisDeformations.WLift.IsLift.half_zero
{Λ : Type u_1}
[Ring Λ]
[Algebra (ZMod 2) Λ]
{GΛ : GExt.GAlg Λ}
{Λ' : Type u_2}
[Ring Λ']
[Algebra (ZMod 4) Λ']
{GΛ' : GExt.GAlg Λ'}
{π : Λ' →+* Λ}
{M : Type u_3}
[AddCommGroup M]
[Module (ZMod 2) M]
{M' : Type u_4}
[AddCommGroup M']
[Module (ZMod 4) M']
{MM' : GExt.GMod GΛ' M'}
{MM : GExt.GMod GΛ M}
{ρ : M' →+ M}
(H : IsLift MM' MM π ρ)
:
H.half 0 = 0
theorem
MultiplicativeBasisDeformations.WLift.IsLift.half_smul
{Λ : Type u_1}
[Ring Λ]
[Algebra (ZMod 2) Λ]
{GΛ : GExt.GAlg Λ}
{Λ' : Type u_2}
[Ring Λ']
[Algebra (ZMod 4) Λ']
{GΛ' : GExt.GAlg Λ'}
{π : Λ' →+* Λ}
{M : Type u_3}
[AddCommGroup M]
[Module (ZMod 2) M]
{M' : Type u_4}
[AddCommGroup M']
[Module (ZMod 4) M']
{MM' : GExt.GMod GΛ' M'}
{MM : GExt.GMod GΛ M}
{ρ : M' →+ M}
(H : IsLift MM' MM π ρ)
(a : ZMod 4)
{m : M'}
(hm : ρ m = 0)
:
theorem
MultiplicativeBasisDeformations.WLift.IsLift.half_two_smul
{Λ : Type u_1}
[Ring Λ]
[Algebra (ZMod 2) Λ]
{GΛ : GExt.GAlg Λ}
{Λ' : Type u_2}
[Ring Λ']
[Algebra (ZMod 4) Λ']
{GΛ' : GExt.GAlg Λ'}
{π : Λ' →+* Λ}
{M : Type u_3}
[AddCommGroup M]
[Module (ZMod 2) M]
{M' : Type u_4}
[AddCommGroup M']
[Module (ZMod 4) M']
{MM' : GExt.GMod GΛ' M'}
{MM : GExt.GMod GΛ M}
{ρ : M' →+ M}
(H : IsLift MM' MM π ρ)
(m : M')
:
H.half (2 • m) = ρ m
theorem
MultiplicativeBasisDeformations.WLift.IsLift.half_deg
{Λ : Type u_1}
[Ring Λ]
[Algebra (ZMod 2) Λ]
{GΛ : GExt.GAlg Λ}
{Λ' : Type u_2}
[Ring Λ']
[Algebra (ZMod 4) Λ']
{GΛ' : GExt.GAlg Λ'}
{π : Λ' →+* Λ}
{M : Type u_3}
[AddCommGroup M]
[Module (ZMod 2) M]
{M' : Type u_4}
[AddCommGroup M']
[Module (ZMod 4) M']
{MM' : GExt.GMod GΛ' M'}
{MM : GExt.GMod GΛ M}
{ρ : M' →+ M}
(H : IsLift MM' MM π ρ)
{p : ℤ}
{m : M'}
(hm : MM'.gr.IsHom p m)
(h0 : ρ m = 0)
:
theorem
MultiplicativeBasisDeformations.WLift.IsLift.half_act
{Λ : Type u_1}
[Ring Λ]
[Algebra (ZMod 2) Λ]
{GΛ : GExt.GAlg Λ}
{Λ' : Type u_2}
[Ring Λ']
[Algebra (ZMod 4) Λ']
{GΛ' : GExt.GAlg Λ'}
{π : Λ' →+* Λ}
{M : Type u_3}
[AddCommGroup M]
[Module (ZMod 2) M]
{M' : Type u_4}
[AddCommGroup M']
[Module (ZMod 4) M']
{MM' : GExt.GMod GΛ' M'}
{MM : GExt.GMod GΛ M}
{ρ : M' →+ M}
(H : IsLift MM' MM π ρ)
{m : M'}
(h0 : ρ m = 0)
(b : Λ')
:
Lifting maps #
theorem
MultiplicativeBasisDeformations.WLift.half_indep
{Λ : Type u_1}
[Ring Λ]
[Algebra (ZMod 2) Λ]
{GΛ : GExt.GAlg Λ}
{Λ' : Type u_2}
[Ring Λ']
[Algebra (ZMod 4) Λ']
{GΛ' : GExt.GAlg Λ'}
{π : Λ' →+* Λ}
{M : Type u_3}
[AddCommGroup M]
[Module (ZMod 2) M]
{M' : Type u_4}
[AddCommGroup M']
[Module (ZMod 4) M']
{MM' : GExt.GMod GΛ' M'}
{MM : GExt.GMod GΛ M}
{ρM : M' →+ M}
{N : Type u_5}
[AddCommGroup N]
[Module (ZMod 2) N]
{N' : Type u_6}
[AddCommGroup N']
[Module (ZMod 4) N']
{NN' : GExt.GMod GΛ' N'}
{NN : GExt.GMod GΛ N}
{ρN : N' →+ N}
(hπ : IsRed GΛ' GΛ π)
(HM : IsLift MM' MM π ρM)
(HN : IsLift NN' NN π ρN)
(E : M' →ₗ[ZMod 4] Λ' →ₗ[ZMod 4] N')
(hE : ∀ (m : M') (b : Λ'), ρN ((E m) b) = 0)
{m₁ m₂ : M'}
{b₁ b₂ : Λ'}
(hm : ρM m₁ = ρM m₂)
(hb : π b₁ = π b₂)
:
noncomputable def
MultiplicativeBasisDeformations.WLift.halfBil
{Λ : Type u_1}
[Ring Λ]
[Algebra (ZMod 2) Λ]
{GΛ : GExt.GAlg Λ}
{Λ' : Type u_2}
[Ring Λ']
[Algebra (ZMod 4) Λ']
{GΛ' : GExt.GAlg Λ'}
{π : Λ' →+* Λ}
{M : Type u_3}
[AddCommGroup M]
[Module (ZMod 2) M]
{M' : Type u_4}
[AddCommGroup M']
[Module (ZMod 4) M']
{MM' : GExt.GMod GΛ' M'}
{MM : GExt.GMod GΛ M}
{ρM : M' →+ M}
{N : Type u_5}
[AddCommGroup N]
[Module (ZMod 2) N]
{N' : Type u_6}
[AddCommGroup N']
[Module (ZMod 4) N']
{NN' : GExt.GMod GΛ' N'}
{NN : GExt.GMod GΛ N}
{ρN : N' →+ N}
(hπ : IsRed GΛ' GΛ π)
(HM : IsLift MM' MM π ρM)
(HN : IsLift NN' NN π ρN)
(E : M' →ₗ[ZMod 4] Λ' →ₗ[ZMod 4] N')
(hE : ∀ (m : M') (b : Λ'), ρN ((E m) b) = 0)
(a : Λ)
:
M →ₗ[ZMod 2] N
Halving a bilinear map with values in the kernel of the reduction.
Instances For
theorem
MultiplicativeBasisDeformations.WLift.halfBil_spec
{Λ : Type u_1}
[Ring Λ]
[Algebra (ZMod 2) Λ]
{GΛ : GExt.GAlg Λ}
{Λ' : Type u_2}
[Ring Λ']
[Algebra (ZMod 4) Λ']
{GΛ' : GExt.GAlg Λ'}
{π : Λ' →+* Λ}
{M : Type u_3}
[AddCommGroup M]
[Module (ZMod 2) M]
{M' : Type u_4}
[AddCommGroup M']
[Module (ZMod 4) M']
{MM' : GExt.GMod GΛ' M'}
{MM : GExt.GMod GΛ M}
{ρM : M' →+ M}
{N : Type u_5}
[AddCommGroup N]
[Module (ZMod 2) N]
{N' : Type u_6}
[AddCommGroup N']
[Module (ZMod 4) N']
{NN' : GExt.GMod GΛ' N'}
{NN : GExt.GMod GΛ N}
{ρN : N' →+ N}
(hπ : IsRed GΛ' GΛ π)
(HM : IsLift MM' MM π ρM)
(HN : IsLift NN' NN π ρN)
(E : M' →ₗ[ZMod 4] Λ' →ₗ[ZMod 4] N')
(hE : ∀ (m : M') (b : Λ'), ρN ((E m) b) = 0)
(m : M')
(b : Λ')
:
theorem
MultiplicativeBasisDeformations.WLift.halfBil_add
{Λ : Type u_1}
[Ring Λ]
[Algebra (ZMod 2) Λ]
{GΛ : GExt.GAlg Λ}
{Λ' : Type u_2}
[Ring Λ']
[Algebra (ZMod 4) Λ']
{GΛ' : GExt.GAlg Λ'}
{π : Λ' →+* Λ}
{M : Type u_3}
[AddCommGroup M]
[Module (ZMod 2) M]
{M' : Type u_4}
[AddCommGroup M']
[Module (ZMod 4) M']
{MM' : GExt.GMod GΛ' M'}
{MM : GExt.GMod GΛ M}
{ρM : M' →+ M}
{N : Type u_5}
[AddCommGroup N]
[Module (ZMod 2) N]
{N' : Type u_6}
[AddCommGroup N']
[Module (ZMod 4) N']
{NN' : GExt.GMod GΛ' N'}
{NN : GExt.GMod GΛ N}
{ρN : N' →+ N}
(hπ : IsRed GΛ' GΛ π)
(HM : IsLift MM' MM π ρM)
(HN : IsLift NN' NN π ρN)
(E : M' →ₗ[ZMod 4] Λ' →ₗ[ZMod 4] N')
(hE : ∀ (m : M') (b : Λ'), ρN ((E m) b) = 0)
(a a' : Λ)
:
theorem
MultiplicativeBasisDeformations.WLift.halfBil_smul
{Λ : Type u_1}
[Ring Λ]
[Algebra (ZMod 2) Λ]
{GΛ : GExt.GAlg Λ}
{Λ' : Type u_2}
[Ring Λ']
[Algebra (ZMod 4) Λ']
{GΛ' : GExt.GAlg Λ'}
{π : Λ' →+* Λ}
{M : Type u_3}
[AddCommGroup M]
[Module (ZMod 2) M]
{M' : Type u_4}
[AddCommGroup M']
[Module (ZMod 4) M']
{MM' : GExt.GMod GΛ' M'}
{MM : GExt.GMod GΛ M}
{ρM : M' →+ M}
{N : Type u_5}
[AddCommGroup N]
[Module (ZMod 2) N]
{N' : Type u_6}
[AddCommGroup N']
[Module (ZMod 4) N']
{NN' : GExt.GMod GΛ' N'}
{NN : GExt.GMod GΛ N}
{ρN : N' →+ N}
(hπ : IsRed GΛ' GΛ π)
(HM : IsLift MM' MM π ρM)
(HN : IsLift NN' NN π ρN)
(E : M' →ₗ[ZMod 4] Λ' →ₗ[ZMod 4] N')
(hE : ∀ (m : M') (b : Λ'), ρN ((E m) b) = 0)
(c : ZMod 2)
(a : Λ)
:
theorem
MultiplicativeBasisDeformations.WLift.halfBil_deg
{Λ : Type u_1}
[Ring Λ]
[Algebra (ZMod 2) Λ]
{GΛ : GExt.GAlg Λ}
{Λ' : Type u_2}
[Ring Λ']
[Algebra (ZMod 4) Λ']
{GΛ' : GExt.GAlg Λ'}
{π : Λ' →+* Λ}
{M : Type u_3}
[AddCommGroup M]
[Module (ZMod 2) M]
{M' : Type u_4}
[AddCommGroup M']
[Module (ZMod 4) M']
{MM' : GExt.GMod GΛ' M'}
{MM : GExt.GMod GΛ M}
{ρM : M' →+ M}
{N : Type u_5}
[AddCommGroup N]
[Module (ZMod 2) N]
{N' : Type u_6}
[AddCommGroup N']
[Module (ZMod 4) N']
{NN' : GExt.GMod GΛ' N'}
{NN : GExt.GMod GΛ N}
{ρN : N' →+ N}
(hπ : IsRed GΛ' GΛ π)
(HM : IsLift MM' MM π ρM)
(HN : IsLift NN' NN π ρN)
(E : M' →ₗ[ZMod 4] Λ' →ₗ[ZMod 4] N')
(hE : ∀ (m : M') (b : Λ'), ρN ((E m) b) = 0)
{t : ℤ}
(hEd : ∀ (p q : ℤ) (m : M') (b : Λ'), MM'.gr.IsHom p m → GΛ'.gr.IsHom q b → NN'.gr.IsHom (p + q + t) ((E m) b))
{p q : ℤ}
{a : Λ}
{m : M}
(ha : GΛ.gr.IsHom q a)
(hm : MM.gr.IsHom p m)
:
noncomputable def
MultiplicativeBasisDeformations.WLift.twMap
{Λ : Type u_1}
[Ring Λ]
[Algebra (ZMod 2) Λ]
{GΛ : GExt.GAlg Λ}
{Λ' : Type u_2}
[Ring Λ']
[Algebra (ZMod 4) Λ']
{GΛ' : GExt.GAlg Λ'}
{π : Λ' →+* Λ}
{M : Type u_3}
[AddCommGroup M]
[Module (ZMod 2) M]
{M' : Type u_4}
[AddCommGroup M']
[Module (ZMod 4) M']
{MM' : GExt.GMod GΛ' M'}
{MM : GExt.GMod GΛ M}
{ρM : M' →+ M}
{N : Type u_5}
[AddCommGroup N]
[Module (ZMod 2) N]
{N' : Type u_6}
[AddCommGroup N']
[Module (ZMod 4) N']
{NN' : GExt.GMod GΛ' N'}
{NN : GExt.GMod GΛ N}
{ρN : N' →+ N}
(HM : IsLift MM' MM π ρM)
(HN : IsLift NN' NN π ρN)
(φ : M →ₗ[ZMod 2] N)
:
M' →ₗ[ZMod 4] N'
The O-linear map tw ∘ φ ∘ ρ.
Instances For
theorem
MultiplicativeBasisDeformations.WLift.twMap_apply
{Λ : Type u_1}
[Ring Λ]
[Algebra (ZMod 2) Λ]
{GΛ : GExt.GAlg Λ}
{Λ' : Type u_2}
[Ring Λ']
[Algebra (ZMod 4) Λ']
{GΛ' : GExt.GAlg Λ'}
{π : Λ' →+* Λ}
{M : Type u_3}
[AddCommGroup M]
[Module (ZMod 2) M]
{M' : Type u_4}
[AddCommGroup M']
[Module (ZMod 4) M']
{MM' : GExt.GMod GΛ' M'}
{MM : GExt.GMod GΛ M}
{ρM : M' →+ M}
{N : Type u_5}
[AddCommGroup N]
[Module (ZMod 2) N]
{N' : Type u_6}
[AddCommGroup N']
[Module (ZMod 4) N']
{NN' : GExt.GMod GΛ' N'}
{NN : GExt.GMod GΛ N}
{ρN : N' →+ N}
(HM : IsLift MM' MM π ρM)
(HN : IsLift NN' NN π ρN)
(φ : M →ₗ[ZMod 2] N)
(m : M')
:
theorem
MultiplicativeBasisDeformations.WLift.exists_liftHom
{Λ : Type u_1}
[Ring Λ]
[Algebra (ZMod 2) Λ]
{GΛ : GExt.GAlg Λ}
{Λ' : Type u_2}
[Ring Λ']
[Algebra (ZMod 4) Λ']
{GΛ' : GExt.GAlg Λ'}
{π : Λ' →+* Λ}
{M : Type u_3}
[AddCommGroup M]
[Module (ZMod 2) M]
{M' : Type u_4}
[AddCommGroup M']
[Module (ZMod 4) M']
{MM' : GExt.GMod GΛ' M'}
{MM : GExt.GMod GΛ M}
{ρM : M' →+ M}
{N : Type u_5}
[AddCommGroup N]
[Module (ZMod 2) N]
{N' : Type u_6}
[AddCommGroup N']
[Module (ZMod 4) N']
{NN' : GExt.GMod GΛ' N'}
{NN : GExt.GMod GΛ N}
{ρN : N' →+ N}
(hπ : IsRed GΛ' GΛ π)
(HM : IsLift MM' MM π ρM)
(HN : IsLift NN' NN π ρN)
(f : M →ₗ[ZMod 2] N)
(hf : ∀ (m : M) (a : Λ), f ((MM.act m) a) = (NN.act (f m)) a)
{d : ℤ}
(hExt : GExt.ExtVanish MM NN 0 d)
(f₀ : M' →ₗ[ZMod 4] N')
(hf₀ : ∀ (m : M'), ρN (f₀ m) = f (ρM m))
(hf₀d : ∀ (p : ℤ) (m : M'), MM'.gr.IsHom p m → NN'.gr.IsHom (p + d) (f₀ m))
:
Lifting maps (Ext¹ vanishing): an A-linear map of degree d between modules with
lifts has a lift of degree d, starting from any 𝒪-linear lift.