Embedding conditionally linear presentations in a larger register

Extending a presentation by zero along an injection preserves its evaluation, marginal, factor and linear-map queries. This puts the graph and content parts of detyping on disjoint registers without changing their query interfaces.

def MIPRE.CL.pull {F : Type u_1} {ι : Type u_2} {κ : Type u_3} (e : ι ↪ κ) (x : κ → F) : ι → F

Read the coordinates in the image of an embedding.

Equations

• MIPRE.CL.pull e x i = x (e i)

noncomputable def MIPRE.CL.push {F : Type u_1} {ι : Type u_2} {κ : Type u_3} [Semiring F] (e : ι ↪ κ) (x : ι → F) : κ → F

Extend by zero outside the image of an embedding.

Equations

• MIPRE.CL.push e x j = if h : ∃ (i : ι), e i = j then x h.choose else 0

@[simp]

theorem MIPRE.CL.push_apply {F : Type u_1} {ι : Type u_2} {κ : Type u_3} [Semiring F] [DecidableEq ι] [DecidableEq κ] (e : ι ↪ κ) (x : ι → F) (i : ι) : push e x (e i) = x i

@[simp]

theorem MIPRE.CL.pull_push {F : Type u_1} {ι : Type u_2} {κ : Type u_3} [Semiring F] [DecidableEq ι] [DecidableEq κ] (e : ι ↪ κ) (x : ι → F) : pull e (push e x) = x

@[simp]

theorem MIPRE.CL.push_zero {F : Type u_1} {ι : Type u_2} {κ : Type u_3} [Semiring F] [DecidableEq ι] [DecidableEq κ] (e : ι ↪ κ) : push e 0 = 0

@[simp]

theorem MIPRE.CL.push_add {F : Type u_1} {ι : Type u_2} {κ : Type u_3} [Semiring F] [DecidableEq ι] [DecidableEq κ] (e : ι ↪ κ) (x y : ι → F) : push e (x + y) = push e x + push e y

@[simp]

theorem MIPRE.CL.pull_add {F : Type u_1} {ι : Type u_2} {κ : Type u_3} [Semiring F] [DecidableEq ι] [DecidableEq κ] (e : ι ↪ κ) (x y : κ → F) : pull e (x + y) = pull e x + pull e y

@[simp]

theorem MIPRE.CL.pull_zero {F : Type u_1} {ι : Type u_2} {κ : Type u_3} [Semiring F] [DecidableEq ι] [DecidableEq κ] (e : ι ↪ κ) : pull e 0 = 0

@[simp]

theorem MIPRE.CL.push_inl_left {F : Type u_1} {ι : Type u_2} {κ : Type u_3} [Semiring F] [DecidableEq ι] [DecidableEq κ] (x : ι → F) (i : ι) : push Function.Embedding.inl x (Sum.inl i) = x i

@[simp]

theorem MIPRE.CL.push_inr_right {F : Type u_1} {ι : Type u_2} {κ : Type u_3} [Semiring F] [DecidableEq ι] [DecidableEq κ] (x : κ → F) (j : κ) : push Function.Embedding.inr x (Sum.inr j) = x j

@[simp]

theorem MIPRE.CL.push_inl_right {F : Type u_1} {ι : Type u_2} {κ : Type u_3} [Semiring F] [DecidableEq ι] [DecidableEq κ] (x : ι → F) (j : κ) : push Function.Embedding.inl x (Sum.inr j) = 0

@[simp]

theorem MIPRE.CL.push_inr_left {F : Type u_1} {ι : Type u_2} {κ : Type u_3} [Semiring F] [DecidableEq ι] [DecidableEq κ] (x : κ → F) (i : ι) : push Function.Embedding.inr x (Sum.inl i) = 0

theorem MIPRE.CL.pull_proj {F : Type u_1} {ι : Type u_2} {κ : Type u_3} [Semiring F] [DecidableEq ι] [DecidableEq κ] (e : ι ↪ κ) (S : Finset ι) (x : κ → F) : pull e ((proj (Finset.map e S)) x) = (proj S) (pull e x)

Restriction of the projection onto an embedded register.

theorem MIPRE.CL.pull_proj_compl {F : Type u_1} {ι : Type u_2} {κ : Type u_3} [Semiring F] [DecidableEq ι] [DecidableEq κ] [Fintype ι] [Fintype κ] (e : ι ↪ κ) (S : Finset ι) (x : κ → F) : pull e ((proj (Finset.map e S)ᶜ) x) = (proj Sᶜ) (pull e x)

Restriction of the projection onto the remaining registers.

theorem MIPRE.CL.proj_push {F : Type u_1} {ι : Type u_2} {κ : Type u_3} [Semiring F] [DecidableEq ι] [DecidableEq κ] (e : ι ↪ κ) (S : Finset ι) (x : ι → F) : (proj (Finset.map e S)) (push e x) = push e ((proj S) x)

Projection commutes with extension by zero.

noncomputable def MIPRE.CL.RegLinear.embed {F : Type u_1} {ι : Type u_2} {κ : Type u_3} [Semiring F] [DecidableEq ι] [DecidableEq κ] (e : ι ↪ κ) {S : Finset ι} (L : RegLinear F S) : RegLinear F (Finset.map e S)

The same register-linear operation on an embedded register.

Equations

• MIPRE.CL.RegLinear.embed e L = { toLinearMap := { toFun := fun (x : κ → F) => MIPRE.CL.push e (L (MIPRE.CL.pull e x)), map_add' := ⋯, map_smul' := ⋯ }, proj_comp_proj' := ⋯ }

@[simp]

theorem MIPRE.CL.RegLinear.embed_apply {F : Type u_1} {ι : Type u_2} {κ : Type u_3} [Semiring F] [DecidableEq ι] [DecidableEq κ] (e : ι ↪ κ) {S : Finset ι} (L : RegLinear F S) (x : κ → F) : (embed e L) x = push e (L (pull e x))

def MIPRE.CL.CLFun.embed {F : Type u_1} {ι : Type u_2} {κ : Type u_3} [Semiring F] [DecidableEq ι] [DecidableEq κ] (e : ι ↪ κ) {ℓ : ℕ} : CLFun F ι ℓ → CLFun F κ ℓ

Extend every factor and map of a presentation along a coordinate injection.

Equations

• MIPRE.CL.CLFun.embed e MIPRE.CL.CLFun.zero = MIPRE.CL.CLFun.zero
• MIPRE.CL.CLFun.embed e (MIPRE.CL.CLFun.cons S L next) = MIPRE.CL.CLFun.cons (Finset.map e S) (MIPRE.CL.RegLinear.embed e L) fun (x : κ → F) => MIPRE.CL.CLFun.embed e (next (MIPRE.CL.pull e x))

theorem MIPRE.CL.CLFun.ExactlyOn.embed {F : Type u_1} {ι : Type u_2} {κ : Type u_3} [Semiring F] [DecidableEq ι] [DecidableEq κ] {ℓ : ℕ} (e : ι ↪ κ) {P : CLFun F ι ℓ} {S : Finset ι} (hP : P.ExactlyOn S) : (CLFun.embed e P).ExactlyOn (Finset.map e S)

Embedded factors still partition precisely the embedded original register.

theorem MIPRE.CL.CLFun.eval_embed {F : Type u_1} {ι : Type u_2} {κ : Type u_3} [Semiring F] [DecidableEq ι] [DecidableEq κ] {ℓ : ℕ} [Fintype ι] [Fintype κ] (e : ι ↪ κ) (P : CLFun F ι ℓ) (x : κ → F) : (embed e P).eval x = push e (P.eval (pull e x))

The embedded CL function acts only on its original coordinates.

theorem MIPRE.CL.CLFun.eval_truncate_embed {F : Type u_1} {ι : Type u_2} {κ : Type u_3} [Semiring F] [DecidableEq ι] [DecidableEq κ] {ℓ : ℕ} [Fintype ι] [Fintype κ] (e : ι ↪ κ) (P : CLFun F ι ℓ) (j : ℕ) (x : κ → F) : (truncate j (embed e P)).eval x = push e ((truncate j P).eval (pull e x))

Marginal queries are transported by the same coordinate embedding.

theorem MIPRE.CL.CLFun.factorOfPrefix_embed {F : Type u_1} {ι : Type u_2} {κ : Type u_3} [Semiring F] [DecidableEq ι] [DecidableEq κ] {ℓ : ℕ} [Fintype ι] [Fintype κ] (e : ι ↪ κ) (P : CLFun F ι ℓ) (j : ℕ) (x : κ → F) : (embed e P).factorOfPrefix j x = Finset.map e (P.factorOfPrefix j (pull e x))

Factor queries from an arbitrary prefix commute with embedding.

theorem MIPRE.CL.CLFun.mapOfPrefix_embed {F : Type u_1} {ι : Type u_2} {κ : Type u_3} [Semiring F] [DecidableEq ι] [DecidableEq κ] {ℓ : ℕ} [Fintype ι] [Fintype κ] (e : ι ↪ κ) (P : CLFun F ι ℓ) (j : ℕ) (x y : κ → F) : ((embed e P).mapOfPrefix j x) y = push e ((P.mapOfPrefix j (pull e x)) (pull e y))

Linear-map queries from an arbitrary prefix commute with embedding.