Lax Lean Archive

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

Well-defined channel contractions on projected tensor spaces

Lax342547.TensorContractions · concepts/Lax342547/TensorContractions.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

    Two channel evaluation maps on the tensor factors determine a unique linear contraction on their matrix tensor space. Its value is independent of how the maps are extended to the ambient coefficient space.

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

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

    1 ambient_outer proven

    2 contraction_outer proven

    3 contraction_unique proven

    4 extension_agreement proven

    Lean source view on GitHub

    1import Lax342547.ProjectedPins
    2import Lax342547.ConcreteGeometry
    3import Mathlib.LinearAlgebra.Basis.VectorSpace
    4
    5/-!
    6---
    7title: Well-defined channel contractions on projected tensor spaces
    8type: lemma
    9---
    10Two channel evaluation maps on the tensor factors determine a unique
    11linear contraction on their matrix tensor space. Its value is independent
    12of how the maps are extended to the ambient coefficient space.
    13-/
    14
    15namespace Lax342547.TensorContractions
    16
    17open Lax342547.MomentSpace Lax342547.ProjectedPins Lax342547.ConcreteGeometry
    18
    19variable {B H : Type} [Fintype B] [Fintype H]
    20
    21noncomputable def ambient (f g : (B → Binary) →ₗ[Binary] (H → Binary)) :
    22 Matrix B B Binary →ₗ[Binary] Binary := by
    23 classical
    24 exact matrixPair (LinearMap.BilinForm.toMatrix' ((dotProductBilin Binary Binary).compl₁₂ f g))
    25
    26noncomputable def extend {S : Submodule Binary (B → Binary)} (f : S →ₗ[Binary] (H → Binary)) :
    27 (B → Binary) →ₗ[Binary] (H → Binary) := Classical.choose f.exists_extend
    28
    29def tensor {S T : Submodule Binary (B → Binary)} (v : S) (w : T) : tensorSpace S T :=
    30 ⟨Matrix.vecMulVec v.val w.val, Submodule.subset_span ⟨v.val, v.property, w.val, w.property, rfl⟩⟩
    31
    32noncomputable def contraction {S T : Submodule Binary (B → Binary)}
    33 (f : S →ₗ[Binary] (H → Binary)) (g : T →ₗ[Binary] (H → Binary)) :
    34 tensorSpace S T →ₗ[Binary] Binary :=
    35 (ambient (extend f) (extend g)).comp (tensorSpace S T).subtype
    36
    37axiom ambient_outer (f g : (B → Binary) →ₗ[Binary] (H → Binary)) (v w : B → Binary) :
    38 ambient f g (Matrix.vecMulVec v w) = dotProduct (f v) (g w)
    39
    40axiom contraction_outer {S T : Submodule Binary (B → Binary)}
    41 (f : S →ₗ[Binary] (H → Binary)) (g : T →ₗ[Binary] (H → Binary)) (v : S) (w : T) :
    42 contraction f g (tensor v w) = dotProduct (f v) (g w)
    43
    44axiom extension_agreement {S T : Submodule Binary (B → Binary)}
    45 (f : S →ₗ[Binary] (H → Binary)) (g : T →ₗ[Binary] (H → Binary))
    46 (f' g' : (B → Binary) →ₗ[Binary] (H → Binary))
    47 (hf : f'.comp S.subtype = f) (hg : g'.comp T.subtype = g) (M : tensorSpace S T) :
    48 contraction f g M = ambient f' g' M.val
    49
    50axiom contraction_unique {S T : Submodule Binary (B → Binary)}
    51 (f : S →ₗ[Binary] (H → Binary)) (g : T →ₗ[Binary] (H → Binary))
    52 (c : tensorSpace S T →ₗ[Binary] Binary)
    53 (hc : ∀ (v : S) (w : T), c (tensor v w) = dotProduct (f v) (g w)) :
    54 c = contraction f g
    55
    56end Lax342547.TensorContractions
    57
    Show ProofShow 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…