Twice a first-order lift #
integral-deformations.tex (proof of Lemma 10.2): "take module and map corrections for
a first-order 𝔽₂-cocycle and use twice their lifts over 𝒪. Every equation is linear in ε;
multiplication by two makes it depend only on the modulo-two base matrices."
For a cocycle μ̃ = 2μ̄ over 𝒪, a lifted action ν of M for μ̄ gives the lifted action
2ν of a lift M̃ (actLiftTw), and a lifted map (f, g) gives (f̃, 2g) (isLiftHom_tw).
twMap #
theorem
MultiplicativeBasisDeformations.WLift.twMap_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}
(HM : IsLift MM' MM π ρM)
(HN : IsLift NN' NN π ρN)
(φ ψ : M →ₗ[ZMod 2] N)
:
theorem
MultiplicativeBasisDeformations.WLift.twMap_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' →+ 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)
:
theorem
MultiplicativeBasisDeformations.WLift.twMap_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}
(HM : IsLift MM' MM π ρM)
(HN : IsLift NN' NN π ρN)
(t : ZMod 2)
(φ : M →ₗ[ZMod 2] N)
:
theorem
MultiplicativeBasisDeformations.WLift.twMap_red_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}
(HM : IsLift MM' MM π ρM)
(HN : IsLift NN' NN π ρN)
(a : ZMod 4)
(φ : M →ₗ[ZMod 2] N)
:
theorem
MultiplicativeBasisDeformations.WLift.twMap_sum
{Λ : 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)
{κ : Type u_7}
(s : Finset κ)
(φ : κ → M →ₗ[ZMod 2] N)
:
theorem
MultiplicativeBasisDeformations.WLift.twMap_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' →+ 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)
:
twMap HM HN 0 = 0
theorem
MultiplicativeBasisDeformations.WLift.lift_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' →+ 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)
{f : M →ₗ[ZMod 2] N}
{f' : M' →ₗ[ZMod 4] N'}
(hf' : ∀ (m : M'), ρN (f' m) = f (ρM m))
(v : M)
:
A lift of a map commutes with twice.
theorem
MultiplicativeBasisDeformations.WLift.comp_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)
{P : Type u_7}
[AddCommGroup P]
[Module (ZMod 2) P]
{P' : Type u_8}
[AddCommGroup P']
[Module (ZMod 4) P']
{PP' : GExt.GMod GΛ' P'}
{PP : GExt.GMod GΛ P}
{ρP : P' →+ P}
(HP : IsLift PP' PP π ρP)
{f : N →ₗ[ZMod 2] P}
{f' : N' →ₗ[ZMod 4] P'}
(hf' : ∀ (m : N'), ρP (f' m) = f (ρN m))
(g : M →ₗ[ZMod 2] N)
:
theorem
MultiplicativeBasisDeformations.WLift.twMap_comp
{Λ : 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)
{P : Type u_7}
[AddCommGroup P]
[Module (ZMod 2) P]
{P' : Type u_8}
[AddCommGroup P']
[Module (ZMod 4) P']
{PP' : GExt.GMod GΛ' P'}
{PP : GExt.GMod GΛ P}
{ρP : P' →+ P}
(HP : IsLift PP' PP π ρP)
{f : M →ₗ[ZMod 2] N}
{f' : M' →ₗ[ZMod 4] N'}
(hf' : ∀ (m : M'), ρN (f' m) = f (ρM m))
(g : N →ₗ[ZMod 2] P)
:
Twice a lifted action #
@[reducible, inline]
abbrev
MultiplicativeBasisDeformations.WLift.πs
{Λ : Type u_1}
[Ring Λ]
{Λ' : Type u_2}
[Ring Λ']
{π : Λ' →+* Λ}
(a : ℕ → Λ')
:
ℕ → Λ
The sequence of reductions.
Instances For
theorem
MultiplicativeBasisDeformations.WLift.πs_single
{Λ : Type u_1}
[Ring Λ]
[Algebra (ZMod 2) Λ]
{Λ' : Type u_2}
[Ring Λ']
[Algebra (ZMod 4) Λ']
{π : Λ' →+* Λ}
(b : Λ')
:
πs (GExt.single b) = GExt.single (π b)
noncomputable def
MultiplicativeBasisDeformations.WLift.actLiftTw
{Λ : 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}
(HM : IsLift MM' MM π ρM)
(hπ : IsRed GΛ' GΛ π)
{μ : Λ →ₗ[ZMod 2] Λ →ₗ[ZMod 2] Λ}
{μ' : Λ' →ₗ[ZMod 4] Λ' →ₗ[ZMod 4] Λ'}
(hμ' : ∀ (a b x : Λ'), π x = (μ (π a)) (π b) → (μ' a) b = 2 • x)
{q : ℤ}
(L : GExt.ActLift μ q MM)
:
GExt.ActLift μ' q MM'
Twice a lifted action (integral-deformations.tex).
Instances For
theorem
MultiplicativeBasisDeformations.WLift.actLiftTw_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' →+ M}
(HM : IsLift MM' MM π ρM)
(hπ : IsRed GΛ' GΛ π)
{μ : Λ →ₗ[ZMod 2] Λ →ₗ[ZMod 2] Λ}
{μ' : Λ' →ₗ[ZMod 4] Λ' →ₗ[ZMod 4] Λ'}
(hμ' : ∀ (a b x : Λ'), π x = (μ (π a)) (π b) → (μ' a) b = 2 • x)
{q : ℤ}
(L : GExt.ActLift μ q MM)
(m : M')
(b : Λ')
:
theorem
MultiplicativeBasisDeformations.WLift.isLiftHom_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' →+ 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)
(hπ : IsRed GΛ' GΛ π)
{μ : Λ →ₗ[ZMod 2] Λ →ₗ[ZMod 2] Λ}
{μ' : Λ' →ₗ[ZMod 4] Λ' →ₗ[ZMod 4] Λ'}
(hμ' : ∀ (a b x : Λ'), π x = (μ (π a)) (π b) → (μ' a) b = 2 • x)
{q : ℤ}
(L₁ : GExt.ActLift μ q MM)
(L₂ : GExt.ActLift μ q NN)
{f g : M →ₗ[ZMod 2] N}
(h : GExt.IsLiftHom L₁ L₂ f g)
{f' : M' →ₗ[ZMod 4] N'}
(hf'act : ∀ (m : M') (b : Λ'), f' ((MM'.act m) b) = (NN'.act (f' m)) b)
(hf' : ∀ (m : M'), ρN (f' m) = f (ρM m))
:
GExt.IsLiftHom (actLiftTw HM hπ hμ' L₁) (actLiftTw HN hπ hμ' L₂) f' (twMap HM HN g)
Twice a lifted map.