Lax Lean Archive

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

Quotient extractors isolate individual tensor label blocks

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

    A label block is the tensor lift of a base matrix. Bilinear contraction commutes with this lift. Extractors that read one label and kill the others therefore transfer pure annihilation to that base block.

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

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

    1 block_contraction proven

    2 quotient_isolation proven

    Lean source view on GitHub

    1import Lax342547.TensorAnnihilators
    2import Lax342547.SparsePins
    3
    4/-!
    5---
    6title: Quotient extractors isolate individual tensor label blocks
    7type: lemma
    8---
    9A label block is the tensor lift of a base matrix. Bilinear contraction
    10commutes with this lift. Extractors that read one label and kill the
    11others therefore transfer pure annihilation to that base block.
    12-/
    13
    14namespace Lax342547.TensorBlocks
    15
    16open Lax342547.MomentSpace Lax342547.SparsePins Lax342547.ConcreteGeometry
    17open Lax342547.TensorAnnihilators
    18
    19def block {Label Coord Base : Type} (p : Label → Coord → Binary) (s : Label) :
    20 Matrix Base Base Binary →ₗ[Binary] Matrix (Coord × Base) (Coord × Base) Binary where
    21 toFun Z i j := p s i.1 * p s j.1 * Z i.2 j.2
    22 map_add' Z W := by ext i j; exact mul_add _ _ _
    23 map_smul' c Z := by
    24 ext i j
    25 change p s i.1 * p s j.1 * (c * Z i.2 j.2) = c * (p s i.1 * p s j.1 * Z i.2 j.2)
    26 ring
    27
    28axiom block_contraction {Label Coord Base V W : Type} [Fintype Coord] [Fintype Base]
    29 [AddCommGroup V] [Module Binary V] [AddCommGroup W] [Module Binary W]
    30 (p : Label → Coord → Binary) (s : Label) (Z : Matrix Base Base Binary)
    31 (q : (Coord × Base → Binary) →ₗ[Binary] V)
    32 (r : (Coord × Base → Binary) →ₗ[Binary] W)
    33 (β : V →ₗ[Binary] W →ₗ[Binary] Binary) : by
    34 classical
    35 letI : DecidableEq (Coord × Base) := Classical.decEq _
    36 exact matrixPair (LinearMap.BilinForm.toMatrix' (β.compl₁₂ q r)) (block p s Z) =
    37 matrixPair (LinearMap.BilinForm.toMatrix'
    38 (β.compl₁₂ (q.comp (labelTensor p s)) (r.comp (labelTensor p s)))) Z
    39
    40axiom quotient_isolation {Label Coord Base : Type} [Fintype Coord] [Fintype Base]
    41 [DecidableEq Label]
    42 (p : Label → Coord → Binary) (L : Finset Label) (s : Label) (hs : s ∈ L)
    43 (Z : Label → Matrix Base Base Binary)
    44 (S T : Submodule Binary (Coord × Base → Binary))
    45 (A B : Submodule Binary (Base → Binary))
    46 (q : ((Coord × Base → Binary) ⧸ S) →ₗ[Binary] ((Base → Binary) ⧸ A))
    47 (r : ((Coord × Base → Binary) ⧸ T) →ₗ[Binary] ((Base → Binary) ⧸ B))
    48 (hq : ∀ t ∈ L, ∀ v, q (S.mkQ (labelTensor p t v)) = if t = s then A.mkQ v else 0)
    49 (hr : ∀ t ∈ L, ∀ v, r (T.mkQ (labelTensor p t v)) = if t = s then B.mkQ v else 0)
    50 (h : PureAnnihilates (∑ t ∈ L, block p t (Z t)) S T) :
    51 PureAnnihilates (Z s) A B
    52
    53end Lax342547.TensorBlocks
    54
    Show ProofShow Proof
    Builds on
    Used by
    From Mathlib

    none

    Discussion

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

    Loading discussion…