Documentation

MIPRE.Foundations.CL.Register

Register subspaces #

The linear spaces of the conditionally linear machinery (blueprint sec:ps-cl, paper linear.tex) are V = F^ι for a finite index type ι, and the subspaces that occur in it are register subspaces: spans of subsets of the standard basis, hence determined by a set S : Finset ι of coordinates (paper preliminaries.tex, "Register subspace"). This file fixes the two pieces of vocabulary in which everything else is written.

MIPRE.CL.proj S : (ι → F) →ₗ[F] (ι → F) is the coordinate projection onto V_S along the complementary register subspace V_{Sᶜ}: the paper's x ↦ x^{V_S}.
MIPRE.CL.RegLinear F S is a linear map "on V_S", presented as an endomorphism L of the ambient space with proj S ∘ L ∘ proj S = L: it reads only the coordinates in S and writes only there. This is how the paper's L₁ : V₁ → V₁ and L_{k,u} : V_{k,u} → V_{k,u} are handled, and it makes the paper's shorthand x^{L} = L(x^{V_S}) literally L x (RegLinear.apply_proj).

Everything here is elementary; the point is to fix names and simp lemmas.

Coordinate projections #

def MIPRE.CL.proj {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] (S : Finset ι) :

(ι → F) →ₗ[F] ι → F

The coordinate projection onto the register subspace V_S: it keeps the coordinates in S and zeroes the others (the paper's x ↦ x^{V_S}, the projection onto V_S parallel to V_{Sᶜ}).

Equations

MIPRE.CL.proj S = { toFun := fun (x : ι → F) (i : ι) => if i ∈ S then x i else 0, map_add' := ⋯, map_smul' := ⋯ }

Instances For

@[simp]

theorem MIPRE.CL.proj_apply {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] (S : Finset ι) (x : ι → F) (i : ι) :

(proj S) x i = if i ∈ S then x i else 0

theorem MIPRE.CL.proj_apply_of_mem {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] {S : Finset ι} {i : ι} (h : i ∈ S) (x : ι → F) :

(proj S) x i = x i

theorem MIPRE.CL.proj_apply_of_not_mem {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] {S : Finset ι} {i : ι} (h : i ∉ S) (x : ι → F) :

(proj S) x i = 0

@[simp]

theorem MIPRE.CL.proj_proj {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] (S T : Finset ι) (x : ι → F) :

(proj S) ((proj T) x) = (proj (S ∩ T)) x

theorem MIPRE.CL.proj_proj_self {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] (S : Finset ι) (x : ι → F) :

(proj S) ((proj S) x) = (proj S) x

@[simp]

theorem MIPRE.CL.proj_empty {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] (x : ι → F) :

(proj ∅) x = 0

@[simp]

theorem MIPRE.CL.proj_univ {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] [Fintype ι] (x : ι → F) :

(proj Finset.univ) x = x

theorem MIPRE.CL.proj_proj_of_subset {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] {S T : Finset ι} (h : S ⊆ T) (x : ι → F) :

(proj S) ((proj T) x) = (proj S) x

theorem MIPRE.CL.proj_proj_of_subset' {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] {S T : Finset ι} (h : S ⊆ T) (x : ι → F) :

(proj T) ((proj S) x) = (proj S) x

theorem MIPRE.CL.proj_proj_of_disjoint {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] {S T : Finset ι} (h : Disjoint S T) (x : ι → F) :

(proj S) ((proj T) x) = 0

theorem MIPRE.CL.proj_add_proj_compl {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] [Fintype ι] (S : Finset ι) (x : ι → F) :

(proj S) x + (proj Sᶜ) x = x

theorem MIPRE.CL.proj_union_of_disjoint {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] {S T : Finset ι} (h : Disjoint S T) (x : ι → F) :

(proj (S ∪ T)) x = (proj S) x + (proj T) x

theorem MIPRE.CL.proj_eq_self_iff {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] {S : Finset ι} {x : ι → F} :

(proj S) x = x ↔ ∀ i ∉ S, x i = 0

def MIPRE.CL.register {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] (S : Finset ι) :

Submodule F (ι → F)

The register subspace V_S, as a submodule: the vectors vanishing outside S.

Equations

MIPRE.CL.register S = (MIPRE.CL.proj S).range

Instances For

Linear maps on a register subspace #

structure MIPRE.CL.RegLinear (F : Type u_1) [Semiring F] {ι : Type u_2} [DecidableEq ι] (S : Finset ι) :

Type (max u_1 u_2)

A linear map on the register subspace V_S, presented as an endomorphism L of the ambient space with proj S ∘ L ∘ proj S = L: it depends only on the coordinates in S, and its values lie in V_S. This is the paper's L₁ : V₁ → V₁; the paper's shorthand x^{L₁} = L₁(x^{V₁}) is then just L₁ x (RegLinear.apply_proj).

toLinearMap : (ι → F) →ₗ[F] ι → F
The underlying endomorphism of the ambient space.
proj_comp_proj' (x : ι → F) : (proj S) (self.toLinearMap ((proj S) x)) = self.toLinearMap x
L = proj S ∘ L ∘ proj S.

Instances For

@[instance_reducible]

instance MIPRE.CL.RegLinear.instFunLikeForall {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] {S : Finset ι} :

FunLike (RegLinear F S) (ι → F) (ι → F)

Equations

MIPRE.CL.RegLinear.instFunLikeForall = { coe := fun (L : MIPRE.CL.RegLinear F S) => ⇑L.toLinearMap, coe_injective := ⋯ }

instance MIPRE.CL.RegLinear.instLinearMapClassForall {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] {S : Finset ι} :

LinearMapClass (RegLinear F S) F (ι → F) (ι → F)

@[simp]

theorem MIPRE.CL.RegLinear.coe_toLinearMap {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] {S : Finset ι} (L : RegLinear F S) :

⇑L.toLinearMap = ⇑L

@[simp]

theorem MIPRE.CL.RegLinear.toLinearMap_apply {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] {S : Finset ι} (L : RegLinear F S) (x : ι → F) :

L.toLinearMap x = L x

theorem MIPRE.CL.RegLinear.proj_comp_proj {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] {S : Finset ι} (L : RegLinear F S) (x : ι → F) :

(proj S) (L ((proj S) x)) = L x

@[simp]

theorem MIPRE.CL.RegLinear.proj_apply {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] {S : Finset ι} (L : RegLinear F S) (x : ι → F) :

(proj S) (L x) = L x

The values of L lie in V_S.

@[simp]

theorem MIPRE.CL.RegLinear.apply_proj {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] {S : Finset ι} (L : RegLinear F S) (x : ι → F) :

L ((proj S) x) = L x

L reads only the coordinates in S: L(x^{V_S}) = L x.

theorem MIPRE.CL.RegLinear.apply_proj_of_subset {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] {S T : Finset ι} (L : RegLinear F S) (h : S ⊆ T) (x : ι → F) :

L ((proj T) x) = L x

theorem MIPRE.CL.RegLinear.proj_apply_of_subset {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] {S T : Finset ι} (L : RegLinear F S) (h : S ⊆ T) (x : ι → F) :

(proj T) (L x) = L x

theorem MIPRE.CL.RegLinear.apply_proj_of_disjoint {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] {S T : Finset ι} (L : RegLinear F S) (h : Disjoint S T) (x : ι → F) :

L ((proj T) x) = 0

theorem MIPRE.CL.RegLinear.proj_apply_of_disjoint {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] {S T : Finset ι} (L : RegLinear F S) (h : Disjoint T S) (x : ι → F) :

(proj T) (L x) = 0

theorem MIPRE.CL.RegLinear.apply_proj_compl {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] {S : Finset ι} [Fintype ι] (L : RegLinear F S) (x : ι → F) :

L ((proj Sᶜ) x) = 0

theorem MIPRE.CL.RegLinear.proj_compl_apply {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] {S : Finset ι} [Fintype ι] (L : RegLinear F S) (x : ι → F) :

(proj Sᶜ) (L x) = 0

theorem MIPRE.CL.RegLinear.ext {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] {S : Finset ι} {L L' : RegLinear F S} (h : ∀ (x : ι → F), L x = L' x) :

L = L'

theorem MIPRE.CL.RegLinear.ext_iff {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] {S : Finset ι} {L L' : RegLinear F S} :

L = L' ↔ ∀ (x : ι → F), L x = L' x

@[instance_reducible]

instance MIPRE.CL.RegLinear.instZero {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] {S : Finset ι} :

Zero (RegLinear F S)

Equations

MIPRE.CL.RegLinear.instZero = { zero := { toLinearMap := 0, proj_comp_proj' := ⋯ } }

@[simp]

theorem MIPRE.CL.RegLinear.zero_apply {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] {S : Finset ι} (x : ι → F) :

0 x = 0

def MIPRE.CL.RegLinear.id {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] (S : Finset ι) :

The identity of V_S, which is proj S on the ambient space.

Equations

MIPRE.CL.RegLinear.id S = { toLinearMap := MIPRE.CL.proj S, proj_comp_proj' := ⋯ }

Instances For

@[simp]

theorem MIPRE.CL.RegLinear.id_apply {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] {S : Finset ι} (x : ι → F) :

(id S) x = (proj S) x

def MIPRE.CL.RegLinear.ofLinearMap {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] (S : Finset ι) (L : (ι → F) →ₗ[F] ι → F) :

Compress an endomorphism of the ambient space to a map on V_S: proj S ∘ L ∘ proj S.

Equations

MIPRE.CL.RegLinear.ofLinearMap S L = { toLinearMap := MIPRE.CL.proj S ∘ₗ L ∘ₗ MIPRE.CL.proj S, proj_comp_proj' := ⋯ }

Instances For

@[simp]

theorem MIPRE.CL.RegLinear.ofLinearMap_apply {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] {S : Finset ι} (L : (ι → F) →ₗ[F] ι → F) (x : ι → F) :

(ofLinearMap S L) x = (proj S) (L ((proj S) x))

def MIPRE.CL.RegLinear.castLE {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] {S T : Finset ι} (h : S ⊆ T) (L : RegLinear F S) :

A map on V_S is a map on V_T whenever S ⊆ T.

Equations

MIPRE.CL.RegLinear.castLE h L = { toLinearMap := L.toLinearMap, proj_comp_proj' := ⋯ }

Instances For

@[simp]

theorem MIPRE.CL.RegLinear.castLE_apply {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] {S T : Finset ι} (h : S ⊆ T) (L : RegLinear F S) (x : ι → F) :

(castLE h L) x = L x

def MIPRE.CL.RegLinear.directSum {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] {S T : Finset ι} (L : RegLinear F S) (M : RegLinear F T) :

RegLinear F (S ∪ T)

The sum of a map on V_S and a map on V_T, as a map on V_{S ∪ T}: their direct sum when S and T are disjoint.

Equations

L.directSum M = { toLinearMap := L.toLinearMap + M.toLinearMap, proj_comp_proj' := ⋯ }

Instances For

@[simp]

theorem MIPRE.CL.RegLinear.directSum_apply {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] {S T : Finset ι} (L : RegLinear F S) (M : RegLinear F T) (x : ι → F) :

(L.directSum M) x = L x + M x