Regular lifts of cyclic projectives #
integral-deformations.tex: "At projective labels the modules are e_xA^{(4)}."
If a graded module M over Λ is cyclic projective, M ≅ e Λ through a generator u and an
inverse ψ, and e = π ẽ for an idempotent ẽ of Λ̃, then every lift M̃ of M is
ẽΛ̃ through the generator w = ũ ẽ (exists_act_w, eq_zero_of_act_w), with inverse ψ̃
lifting ψ (ψO).
theorem
MultiplicativeBasisDeformations.WLift.four_smul'
{N : Type u_5}
[AddCommGroup N]
[Module (ZMod 4) N]
(m : N)
:
2 • 2 • m = 0
noncomputable def
MultiplicativeBasisDeformations.WLift.wG
{Λ : 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 π ρ)
(e' : Λ')
(u : M)
:
M'
The generator w = ũ ẽ.
Instances For
theorem
MultiplicativeBasisDeformations.WLift.ρ_wG
{Λ : 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 π ρ)
(e' : Λ')
(u : M)
(ψ : M →ₗ[ZMod 2] Λ)
(hψ1 : ∀ (m : M), (MM.act u) (ψ m) = m)
(hψ2 : ∀ (x : Λ), ψ ((MM.act u) x) = π e' * x)
:
ρ (wG H e' u) = u
theorem
MultiplicativeBasisDeformations.WLift.act_wG_e
{Λ : 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 π ρ)
(e' : Λ')
(he' : e' * e' = e')
(u : M)
(b : Λ')
:
theorem
MultiplicativeBasisDeformations.WLift.ρ_act_wG
{Λ : 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 π ρ)
(e' : Λ')
(u : M)
(ψ : M →ₗ[ZMod 2] Λ)
(hψ1 : ∀ (m : M), (MM.act u) (ψ m) = m)
(hψ2 : ∀ (x : Λ), ψ ((MM.act u) x) = π e' * x)
(b : Λ')
:
theorem
MultiplicativeBasisDeformations.WLift.exists_act_wG
{Λ : 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π : IsRed GΛ' GΛ π)
(H : IsLift MM' MM π ρ)
(e' : Λ')
(u : M)
(ψ : M →ₗ[ZMod 2] Λ)
(hψ1 : ∀ (m : M), (MM.act u) (ψ m) = m)
(hψ2 : ∀ (x : Λ), ψ ((MM.act u) x) = π e' * x)
(n : M')
:
theorem
MultiplicativeBasisDeformations.WLift.π_eq_zero_of_wG
{Λ : 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 π ρ)
(e' : Λ')
(u : M)
(ψ : M →ₗ[ZMod 2] Λ)
(hψ1 : ∀ (m : M), (MM.act u) (ψ m) = m)
(hψ2 : ∀ (x : Λ), ψ ((MM.act u) x) = π e' * x)
{b : Λ'}
(hb : e' * b = b)
(h : ρ ((MM'.act (wG H e' u)) b) = 0)
:
π b = 0
theorem
MultiplicativeBasisDeformations.WLift.eq_zero_of_act_wG
{Λ : 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π : IsRed GΛ' GΛ π)
(H : IsLift MM' MM π ρ)
(e' : Λ')
(he' : e' * e' = e')
(u : M)
(ψ : M →ₗ[ZMod 2] Λ)
(hψ1 : ∀ (m : M), (MM.act u) (ψ m) = m)
(hψ2 : ∀ (x : Λ), ψ ((MM.act u) x) = π e' * x)
{b : Λ'}
(hb : e' * b = b)
(h : (MM'.act (wG H e' u)) b = 0)
:
b = 0
noncomputable def
MultiplicativeBasisDeformations.WLift.ψGf
{Λ : 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π : IsRed GΛ' GΛ π)
(H : IsLift MM' MM π ρ)
(e' : Λ')
(u : M)
(ψ : M →ₗ[ZMod 2] Λ)
(hψ1 : ∀ (m : M), (MM.act u) (ψ m) = m)
(hψ2 : ∀ (x : Λ), ψ ((MM.act u) x) = π e' * x)
(n : M')
:
Λ'
The inverse ψ̃ : M̃ → ẽΛ̃.
Instances For
theorem
MultiplicativeBasisDeformations.WLift.ψGf_eq
{Λ : 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π : IsRed GΛ' GΛ π)
(H : IsLift MM' MM π ρ)
(e' : Λ')
(he' : e' * e' = e')
(u : M)
(ψ : M →ₗ[ZMod 2] Λ)
(hψ1 : ∀ (m : M), (MM.act u) (ψ m) = m)
(hψ2 : ∀ (x : Λ), ψ ((MM.act u) x) = π e' * x)
{n : M'}
{b : Λ'}
(h : (MM'.act (wG H e' u)) b = n)
:
ψGf hπ H e' u ψ hψ1 hψ2 n = e' * b
noncomputable def
MultiplicativeBasisDeformations.WLift.ψG
{Λ : 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π : IsRed GΛ' GΛ π)
(H : IsLift MM' MM π ρ)
(e' : Λ')
(he' : e' * e' = e')
(u : M)
(ψ : M →ₗ[ZMod 2] Λ)
(hψ1 : ∀ (m : M), (MM.act u) (ψ m) = m)
(hψ2 : ∀ (x : Λ), ψ ((MM.act u) x) = π e' * x)
:
M' →ₗ[ZMod 4] Λ'
The regular corner M̃ ≅ ẽΛ̃.
Instances For
theorem
MultiplicativeBasisDeformations.WLift.ψG_w
{Λ : 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π : IsRed GΛ' GΛ π)
(H : IsLift MM' MM π ρ)
(e' : Λ')
(he' : e' * e' = e')
(u : M)
(ψ : M →ₗ[ZMod 2] Λ)
(hψ1 : ∀ (m : M), (MM.act u) (ψ m) = m)
(hψ2 : ∀ (x : Λ), ψ ((MM.act u) x) = π e' * x)
(b : Λ')
:
theorem
MultiplicativeBasisDeformations.WLift.w_ψG
{Λ : 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π : IsRed GΛ' GΛ π)
(H : IsLift MM' MM π ρ)
(e' : Λ')
(he' : e' * e' = e')
(u : M)
(ψ : M →ₗ[ZMod 2] Λ)
(hψ1 : ∀ (m : M), (MM.act u) (ψ m) = m)
(hψ2 : ∀ (x : Λ), ψ ((MM.act u) x) = π e' * x)
(n : M')
:
theorem
MultiplicativeBasisDeformations.WLift.π_ψG
{Λ : 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π : IsRed GΛ' GΛ π)
(H : IsLift MM' MM π ρ)
(e' : Λ')
(he' : e' * e' = e')
(u : M)
(ψ : M →ₗ[ZMod 2] Λ)
(hψ1 : ∀ (m : M), (MM.act u) (ψ m) = m)
(hψ2 : ∀ (x : Λ), ψ ((MM.act u) x) = π e' * x)
(n : M')
:
π ((ψG hπ H e' he' u ψ hψ1 hψ2) n) = ψ (ρ n)