Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Primal projections and preservation of effective spaces

Lax342547.ProjectedPins · concepts/Lax342547/ProjectedPins.lean · lax-342547

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Lemma

    Pins can mix endpoints and channels. Their endpoint primal spaces are therefore projections. Enlarging pins preserves these spaces and the cut profiles supported in their tensor products.

    Concept map
    3 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.
    Evidence

    This concept declares 3 statements. Each proof establishes one of them relative to its assumptions.

    1 effective_mono proven

    2 projected_mono proven

    3 projected_rank proven

    Lean source view on GitHub

    1import Lax342547.ExactPins
    2import Mathlib.Data.Matrix.Mul
    3
    4/-!
    5---
    6title: Primal projections and preservation of effective spaces
    7type: lemma
    8---
    9Pins can mix endpoints and channels. Their endpoint primal spaces are
    10therefore projections. Enlarging pins preserves these spaces and the
    11cut profiles supported in their tensor products.
    12-/
    13
    14namespace Lax342547.ProjectedPins
    15
    16open Lax342547.MomentSpace Lax342547.ExactPins
    17
    18def primalProjection {B H : Type} (i : Fin 2) :
    19 ((Fin 2 × (B ⊕ H)) → Binary) →ₗ[Binary] (B → Binary) where
    20 toFun v b := v (i, Sum.inl b)
    21 map_add' _ _ := rfl
    22 map_smul' _ _ := rfl
    23
    24def projected {Comp B H N : Type} (P : Pin (Comp × Bool) (Fin 2 × (B ⊕ H)) N)
    25 (i : Fin 2) (a : Comp × Bool) : Submodule Binary (B → Binary) :=
    26 (P.space a).map (primalProjection i)
    27
    28def tensorSpace {B : Type} (S T : Submodule Binary (B → Binary)) :
    29 Submodule Binary (Matrix B B Binary) :=
    30 Submodule.span Binary {M | ∃ v ∈ S, ∃ w ∈ T, M = Matrix.vecMulVec v w}
    31
    32def effective {Comp B H N : Type} (X : Submodule Binary (Comp → Matrix B B Binary))
    33 (P : Pin (Comp × Bool) (Fin 2 × (B ⊕ H)) N) (i : Fin 2) : Submodule Binary X where
    34 carrier := {x | ∀ e, x.val e ∈ tensorSpace (projected P i (e, true)) (projected P i (e, false))}
    35 zero_mem' := fun _e => (tensorSpace _ _).zero_mem
    36 add_mem' := fun hx hy e => (tensorSpace _ _).add_mem (hx e) (hy e)
    37 smul_mem' := fun c _ hx e => (tensorSpace _ _).smul_mem c (hx e)
    38
    39axiom projected_rank {Comp B H N : Type} [Fintype Comp] [Fintype B] [Fintype H]
    40 (P : Pin (Comp × Bool) (Fin 2 × (B ⊕ H)) N) (i : Fin 2) :
    41 (∑ a, Module.finrank Binary (projected P i a)) ≤ P.rank
    42
    43axiom projected_mono {Comp B H N : Type}
    44 (P Q : Pin (Comp × Bool) (Fin 2 × (B ⊕ H)) N) (h : P.Extends Q) (i : Fin 2) :
    45 ∀ a, projected P i a ≤ projected Q i a
    46
    47axiom effective_mono {Comp B H N : Type} (X : Submodule Binary (Comp → Matrix B B Binary))
    48 (P Q : Pin (Comp × Bool) (Fin 2 × (B ⊕ H)) N) (h : P.Extends Q) (i : Fin 2) :
    49 effective X P i ≤ effective X Q i
    50
    51end Lax342547.ProjectedPins
    52
    Show ProofShow ProofShow Proof
    Builds on
    Used by
    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…