Q2Presentation.Lifting.HeisenbergGroup

source

def Q2Presentation.Lifting.dualOp {Yt : BoundaryFramedTarget} {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (y : Yt.Y) :

Module.Dual (ZMod 2) V →ₗ[ZMod 2] Module.Dual (ZMod 2) V

The dual operator: precomposition with the inverse operator.

Equations

Q2Presentation.Lifting.dualOp Φ y = { toFun := fun (lam : Module.Dual (ZMod 2) V) => lam ∘ₗ Φ.op y⁻¹, map_add' := ⋯, map_smul' := ⋯ }

Instances For

source

theorem Q2Presentation.Lifting.dualOp_apply {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (y : Yt.Y) (lam : Module.Dual (ZMod 2) V) (x : V) :

((dualOp Φ y) lam) x = lam ((Φ.op y⁻¹) x)

source

theorem Q2Presentation.Lifting.dualOp_pair {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (y : Yt.Y) (lam : Module.Dual (ZMod 2) V) (x : V) :

((dualOp Φ y) lam) ((Φ.op y) x) = lam x

Pairing invariance of the transported dual.

source

theorem Q2Presentation.Lifting.dualOp_one {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) :

dualOp Φ 1 = LinearMap.id

source

theorem Q2Presentation.Lifting.dualOp_mul {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (y₁ y₂ : Yt.Y) (lam : Module.Dual (ZMod 2) V) :

(dualOp Φ (y₁ * y₂)) lam = (dualOp Φ y₂) ((dualOp Φ y₁) lam)

source

structure Q2Presentation.Lifting.Heis {Yt : BoundaryFramedTarget} {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) :

Type

The Fox–Heisenberg carrier.

d : V
e : Module.Dual (ZMod 2) V
z : ZMod 2
y : Yt.Y

Instances For

source

def Q2Presentation.Lifting.Heis.mul' {Yt : BoundaryFramedTarget} {V : Type} [AddCommGroup V] [Module (ZMod 2) V] {Φ : OperatorFamily Yt V} (a b : Heis Φ) :

Heis Φ

The right-convention semidirect Heisenberg multiplication.

Equations

a.mul' b = { d := (Φ.op b.y) a.d + b.d, e := (Q2Presentation.Lifting.dualOp Φ b.y) a.e + b.e, z := a.z + b.z + ((Q2Presentation.Lifting.dualOp Φ b.y) a.e) b.d, y := a.y * b.y }

Instances For

source

def Q2Presentation.Lifting.Heis.one' {Yt : BoundaryFramedTarget} {V : Type} [AddCommGroup V] [Module (ZMod 2) V] {Φ : OperatorFamily Yt V} :

Heis Φ

Equations

Q2Presentation.Lifting.Heis.one' = { d := 0, e := 0, z := 0, y := 1 }

Instances For

source

def Q2Presentation.Lifting.Heis.inv' {Yt : BoundaryFramedTarget} {V : Type} [AddCommGroup V] [Module (ZMod 2) V] {Φ : OperatorFamily Yt V} (a : Heis Φ) :

Heis Φ

The inverse: transport back and correct the center.

Equations

a.inv' = { d := (Φ.op a.y⁻¹) a.d, e := (Q2Presentation.Lifting.dualOp Φ a.y⁻¹) a.e, z := a.z + ((Q2Presentation.Lifting.dualOp Φ a.y⁻¹) a.e) ((Φ.op a.y⁻¹) a.d), y := a.y⁻¹ }

Instances For

source

theorem Q2Presentation.Lifting.Heis.ext' {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] {Φ : OperatorFamily Yt V} {a b : Heis Φ} (hd : a.d = b.d) (he : a.e = b.e) (hz : a.z = b.z) (hy : a.y = b.y) :

a = b

source

instance Q2Presentation.Lifting.Heis.instGroup {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] {Φ : OperatorFamily Yt V} :

Group (Heis Φ)

Equations

One or more equations did not get rendered due to their size.

source

theorem Q2Presentation.Lifting.Heis.mul_def {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] {Φ : OperatorFamily Yt V} (a b : Heis Φ) :

a * b = a.mul' b

source

@[simp]

theorem Q2Presentation.Lifting.Heis.mul_d {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] {Φ : OperatorFamily Yt V} (a b : Heis Φ) :

(a * b).d = (Φ.op b.y) a.d + b.d

source

@[simp]

theorem Q2Presentation.Lifting.Heis.mul_e {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] {Φ : OperatorFamily Yt V} (a b : Heis Φ) :

(a * b).e = (dualOp Φ b.y) a.e + b.e

source

@[simp]

theorem Q2Presentation.Lifting.Heis.mul_z {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] {Φ : OperatorFamily Yt V} (a b : Heis Φ) :

(a * b).z = a.z + b.z + ((dualOp Φ b.y) a.e) b.d

source

@[simp]

theorem Q2Presentation.Lifting.Heis.mul_y {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] {Φ : OperatorFamily Yt V} (a b : Heis Φ) :

(a * b).y = a.y * b.y

source

@[simp]

theorem Q2Presentation.Lifting.Heis.one_d {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] {Φ : OperatorFamily Yt V} :

d 1 = 0

source

@[simp]

theorem Q2Presentation.Lifting.Heis.one_e {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] {Φ : OperatorFamily Yt V} :

e 1 = 0

source

@[simp]

theorem Q2Presentation.Lifting.Heis.one_z {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] {Φ : OperatorFamily Yt V} :

z 1 = 0

source

@[simp]

theorem Q2Presentation.Lifting.Heis.one_y {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] {Φ : OperatorFamily Yt V} :

y 1 = 1

source

@[simp]

theorem Q2Presentation.Lifting.Heis.inv_d {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] {Φ : OperatorFamily Yt V} (a : Heis Φ) :

a⁻¹.d = (Φ.op a.y⁻¹) a.d

source

@[simp]

theorem Q2Presentation.Lifting.Heis.inv_e {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] {Φ : OperatorFamily Yt V} (a : Heis Φ) :

a⁻¹.e = (dualOp Φ a.y⁻¹) a.e

source

@[simp]

theorem Q2Presentation.Lifting.Heis.inv_z {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] {Φ : OperatorFamily Yt V} (a : Heis Φ) :

a⁻¹.z = a.z + ((dualOp Φ a.y⁻¹) a.e) ((Φ.op a.y⁻¹) a.d)

source

@[simp]

theorem Q2Presentation.Lifting.Heis.inv_y {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] {Φ : OperatorFamily Yt V} (a : Heis Φ) :

a⁻¹.y = a.y⁻¹

source

def Q2Presentation.Lifting.heisEval {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (n : Gen → V) (φ : Gen → Module.Dual (ZMod 2) V) :

GExpr → Heis Φ

The Fox–Heisenberg evaluation, with the ω₂-power pinned to the target modulus (matching GExpr.eval in Yt.Y and foxShadowGen).

Equations

Q2Presentation.Lifting.heisEval Φ q n φ Q2Presentation.GExpr.one = 1
Q2Presentation.Lifting.heisEval Φ q n φ (Q2Presentation.GExpr.gen a) = { d := n a, e := φ a, z := 0, y := q a }
Q2Presentation.Lifting.heisEval Φ q n φ (u.mul v) = Q2Presentation.Lifting.heisEval Φ q n φ u * Q2Presentation.Lifting.heisEval Φ q n φ v
Q2Presentation.Lifting.heisEval Φ q n φ u.inv = (Q2Presentation.Lifting.heisEval Φ q n φ u)⁻¹
Q2Presentation.Lifting.heisEval Φ q n φ (u.powNat k) = Q2Presentation.Lifting.heisEval Φ q n φ u ^ k
Q2Presentation.Lifting.heisEval Φ q n φ u.powOmega2 = Q2Presentation.Lifting.heisEval Φ q n φ u ^ (Q2Presentation.omega2Mod (Nat.card Yt.Y)).val

Instances For

source

theorem Q2Presentation.Lifting.heis_pow_y {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (a : Heis Φ) (k : ℕ) :

(a ^ k).y = a.y ^ k

Powers project on the group coordinate.

source

theorem Q2Presentation.Lifting.heisEval_y {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (n : Gen → V) (φ : Gen → Module.Dual (ZMod 2) V) (w : GExpr) :

(heisEval Φ q n φ w).y = w.eval q

The group coordinate is the plain evaluation.

source

theorem Q2Presentation.Lifting.heis_pow_d {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (a : Heis Φ) (k : ℕ) :

(a ^ k).d = (∑ i ∈ Finset.range k, Φ.op a.y ^ i) a.d

Powers project on the value coordinate as operator norms.

source

theorem Q2Presentation.Lifting.heisEval_d {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (n : Gen → V) (φ : Gen → Module.Dual (ZMod 2) V) (w : GExpr) :

(heisEval Φ q n φ w).d = foxShadowGen Φ.op q n w

The value coordinate is the Fox shadow.

source

def Q2Presentation.Lifting.betaShadow {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (n : Gen → V) (φ : Gen → Module.Dual (ZMod 2) V) (w : GExpr) :

ZMod 2

The mixed central coordinate — the cup pairing of the word.

Equations

Q2Presentation.Lifting.betaShadow Φ q n φ w = (Q2Presentation.Lifting.heisEval Φ q n φ w).z

Instances For