Proposition 10.1(1): the Hom modules of E₄ are free, and E₄/2E₄ = C⁽²⁾ #
integral-deformations.tex (prop:fixed-integral-companion(1)): "Its Hom modules are
free over 𝒪, and E₄/2E₄ = C⁽²⁾." Here E₄ is the graded Hom category of the lifts
M̃_i of the modules M_i of C⁽²⁾ (ModLift).
For lifts M̃ → M, Ñ → N (IsLift) and a degree d, let H̃_d be the graded Λ̃-module
maps M̃ → Ñ of degree d and H_d the graded Λ-module maps M → N of degree d.
Reduction H̃_d → H_d (redHom) is surjective when Ext¹_d(M, N) = 0 (exists_liftHom),
its kernel is 2H̃_d (ker_redHom), and 2f = 0 forces red f = 0 (redHom_of_two). A
finite ℤ/4-module with such a reduction onto an 𝔽₂-space is free on lifts of a basis
(free_of_red). So H̃_d is free with H̃_d/2H̃_d = H_d (homFree).
Free ℤ/4-modules from reductions #
theorem
MultiplicativeBasisDeformations.WLift.red_eq_zero_iff
(a : ZMod 4)
:
Z4.red a = 0 ↔ a = 0 ∨ a = 2
theorem
MultiplicativeBasisDeformations.WLift.free_of_red
{H' : Type u_1}
{H : Type u_2}
[AddCommGroup H']
[Module (ZMod 4) H']
[AddCommGroup H]
[Module (ZMod 2) H]
{ι : Type u_3}
[Fintype ι]
(b : Module.Basis ι (ZMod 2) H)
(r : H' →+ H)
(hrs : ∀ (a : ZMod 4) (x : H'), r (a • x) = Z4.red a • r x)
(hsurj : Function.Surjective ⇑r)
(hker : ∀ (x : H'), r x = 0 → ∃ (y : H'), x = 2 • y)
(hann : ∀ (x : H'), 2 • x = 0 → r x = 0)
:
∃ (b' : Module.Basis ι (ZMod 4) H'), ∀ (i : ι), r (b' i) = b i
A finite ℤ/4-module reducing onto an 𝔽₂-space with kernel 2H and 2x = 0 ⟹ red x = 0 is free on lifts of a basis.
Reduction of module maps #
def
MultiplicativeBasisDeformations.WLift.homD'
{Λ' : Type u_2}
[Ring Λ']
[Algebra (ZMod 4) Λ']
{GΛ' : GExt.GAlg Λ'}
{M' : Type u_4}
[AddCommGroup M']
[Module (ZMod 4) M']
(MM' : GExt.GMod GΛ' M')
{N' : Type u_6}
[AddCommGroup N']
[Module (ZMod 4) N']
(NN' : GExt.GMod GΛ' N')
(d : ℤ)
:
Submodule (ZMod 4) (M' →ₗ[ZMod 4] N')
H̃_d: the graded Λ̃-module maps M̃ → Ñ of degree d.
Instances For
def
MultiplicativeBasisDeformations.WLift.homD
{Λ : Type u_1}
[Ring Λ]
[Algebra (ZMod 2) Λ]
{GΛ : GExt.GAlg Λ}
{M : Type u_3}
[AddCommGroup M]
[Module (ZMod 2) M]
(MM : GExt.GMod GΛ M)
{N : Type u_5}
[AddCommGroup N]
[Module (ZMod 2) N]
(NN : GExt.GMod GΛ N)
(d : ℤ)
:
Submodule (ZMod 2) (M →ₗ[ZMod 2] N)
H_d: the graded Λ-module maps M → N of degree d.
Instances For
theorem
MultiplicativeBasisDeformations.WLift.redL_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}
(HM : IsLift MM' MM π ρM)
(HN : IsLift NN' NN π ρN)
(f : M' →ₗ[ZMod 4] N')
{m₁ m₂ : M'}
(h : ρM m₁ = ρM m₂)
:
ρN (f m₁) = ρN (f m₂)
noncomputable def
MultiplicativeBasisDeformations.WLift.redL
{Λ : 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 4] N')
:
M →ₗ[ZMod 2] N
The reduction of an 𝒪-linear map M̃ → Ñ, as an 𝔽₂-linear map M → N.
Instances For
theorem
MultiplicativeBasisDeformations.WLift.redL_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}
(HM : IsLift MM' MM π ρM)
(HN : IsLift NN' NN π ρN)
(f : M' →ₗ[ZMod 4] N')
(m : M')
:
(redL HM HN f) (ρM m) = ρN (f m)
theorem
MultiplicativeBasisDeformations.WLift.redL_mem
{Λ : 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)
{d : ℤ}
{f : M' →ₗ[ZMod 4] N'}
(hf : f ∈ homD' MM' NN' d)
:
noncomputable def
MultiplicativeBasisDeformations.WLift.redHom
{Λ : 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)
(d : ℤ)
:
The reduction H̃_d → H_d.
Instances For
theorem
MultiplicativeBasisDeformations.WLift.redHom_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}
(hπ : IsRed GΛ' GΛ π)
(HM : IsLift MM' MM π ρM)
(HN : IsLift NN' NN π ρN)
(d : ℤ)
(f : ↥(homD' MM' NN' d))
(m : M')
:
↑((redHom hπ HM HN d) f) (ρM m) = ρN (↑f m)
theorem
MultiplicativeBasisDeformations.WLift.redHom_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)
(d : ℤ)
(a : ZMod 4)
(f : ↥(homD' MM' NN' d))
:
theorem
MultiplicativeBasisDeformations.WLift.redHom_of_two
{Λ : 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)
(d : ℤ)
(f : ↥(homD' MM' NN' d))
(h : 2 • f = 0)
:
(redHom hπ HM HN d) f = 0
2f = 0 forces red f = 0.
theorem
MultiplicativeBasisDeformations.WLift.redHom_surjective
{Λ : 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)
{d : ℤ}
(hlift : ∀ f ∈ homD MM NN d, ∃ f' ∈ homD' MM' NN' d, ∀ (m : M'), ρN (f' m) = f (ρM m))
:
Function.Surjective ⇑(redHom hπ HM HN d)
Surjectivity of the reduction in a degree where maps lift.
theorem
MultiplicativeBasisDeformations.WLift.ker_redHom
{Λ : 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)
{d : ℤ}
(hlift : ∀ f ∈ homD MM NN d, ∃ f' ∈ homD' MM' NN' d, ∀ (m : M'), ρN (f' m) = f (ρM m))
(f : ↥(homD' MM' NN' d))
(h : (redHom hπ HM HN d) f = 0)
:
∃ (g : ↥(homD' MM' NN' d)), f = 2 • g
The kernel of the reduction is 2H̃_d.
theorem
MultiplicativeBasisDeformations.WLift.homFree
{Λ : 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)
{d : ℤ}
[FiniteDimensional (ZMod 2) ↥(homD MM NN d)]
(hlift : ∀ f ∈ homD MM NN d, ∃ f' ∈ homD' MM' NN' d, ∀ (m : M'), ρN (f' m) = f (ρM m))
:
(∃ (b : Module.Basis (Fin (Module.finrank (ZMod 2) ↥(homD MM NN d))) (ZMod 4) ↥(homD' MM' NN' d)),
∀ (i : Fin (Module.finrank (ZMod 2) ↥(homD MM NN d))),
(redHom hπ HM HN d) (b i) = (Module.finBasis (ZMod 2) ↥(homD MM NN d)) i) ∧ Function.Surjective ⇑(redHom hπ HM HN d) ∧ ∀ (f : ↥(homD' MM' NN' d)), (redHom hπ HM HN d) f = 0 ↔ ∃ (g : ↥(homD' MM' NN' d)), f = 2 • g
Proposition 10.1(1) for one pair of lifts and one degree: if maps of degree d lift,
then H̃_d is free over ℤ/4 on lifts of a basis of H_d, and the reduction H̃_d → H_d is
surjective with kernel 2H̃_d (so H̃_d/2H̃_d = H_d).
theorem
MultiplicativeBasisDeformations.MeshWalk.homD_lift
{V : Type}
[Quiver V]
[Fintype V]
[DecidableEq V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{c : MeshCoefficients (ZMod 2) Q}
{L : CatAlg.LocalFamily (meshFam Q c)}
{D : CatAlg.MeshData (meshFam Q c) L}
[hone : ∀ (x y : V), Subsingleton (x ⟶ y)]
[(x y : V) → Fintype (x ⟶ y)]
[hfd : ∀ (x y : V), FiniteDimensional (ZMod 2) (meshFam Q c x ⟶ meshFam Q c y)]
{R : Type}
[Fintype R]
[DecidableEq R]
{P : RaySys.Mult D.PV R}
(T : TabIso D P)
(J : D.InjData)
(h1 : DegOne D)
(N : (X : V) → ModLift T X)
(X Y : V)
{d : ℤ}
(hd : -2 < d)
(f : CatAlg.Rep D.F0 (meshFam Q c X) →ₗ[ZMod 2] CatAlg.Rep D.F0 (meshFam Q c Y))
:
Maps of degree d > −2 between the evaluated modules lift to the lifts (Ext¹
vanishing, eq. prime-field-ext-vanishing).
theorem
MultiplicativeBasisDeformations.MeshWalk.integralHomFree
{V : Type}
[Quiver V]
[Fintype V]
[DecidableEq V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{c : MeshCoefficients (ZMod 2) Q}
{L : CatAlg.LocalFamily (meshFam Q c)}
{D : CatAlg.MeshData (meshFam Q c) L}
[hone : ∀ (x y : V), Subsingleton (x ⟶ y)]
[(x y : V) → Fintype (x ⟶ y)]
[hfd : ∀ (x y : V), FiniteDimensional (ZMod 2) (meshFam Q c x ⟶ meshFam Q c y)]
{R : Type}
[Fintype R]
[DecidableEq R]
{P : RaySys.Mult D.PV R}
(T : TabIso D P)
(J : D.InjData)
(h1 : DegOne D)
(N : (X : V) → ModLift T X)
(X Y : V)
{d : ℤ}
(hd : -2 < d)
:
(∃ (b :
Module.Basis (Fin (Module.finrank (ZMod 2) ↥(WLift.homD (gmodEv D ⋯ X) (gmodEv D ⋯ Y) d))) (ZMod 4)
↥(WLift.homD' (N X).MM (N Y).MM d)),
∀ (i : Fin (Module.finrank (ZMod 2) ↥(WLift.homD (gmodEv D ⋯ X) (gmodEv D ⋯ Y) d))),
(WLift.redHom ⋯ ⋯ ⋯ d) (b i) = (Module.finBasis (ZMod 2) ↥(WLift.homD (gmodEv D ⋯ X) (gmodEv D ⋯ Y) d)) i) ∧ Function.Surjective ⇑(WLift.redHom ⋯ ⋯ ⋯ d) ∧ ∀ (f : ↥(WLift.homD' (N X).MM (N Y).MM d)),
(WLift.redHom ⋯ ⋯ ⋯ d) f = 0 ↔ ∃ (g : ↥(WLift.homD' (N X).MM (N Y).MM d)), f = 2 • g
Proposition 10.1(1) (prop:fixed-integral-companion(1)): the graded Hom modules of
E₄ (the lifts M̃_X of the modules of C⁽²⁾) are free over 𝒪 = ℤ/4 in every degree
d > −2, and reduction identifies E₄/2E₄ with the graded Hom spaces of the modules of
C⁽²⁾, which are those of C⁽²⁾ by the evaluation of Proposition 2.10.