Lax Lean Archive

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

Paired-frame orbit under the primal and dual actions

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

    Theorem

    Lemma 4.1: two individually injective pairs of frames with equal Gram pairings differ by one ambient linear automorphism, acting contragrediently on the dual frame. No nondegeneracy of the prescribed Gram is needed.

    Concept map
    1 concept; 7 descendants hidden
    100%
    Proven claimThis conceptRelated conceptA → B: B builds on A
    Evidence

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

    1 paired_frame_orbit proven

    2 paired_matrix_orbit proven

    Lean source view on GitHub

    1import Mathlib.LinearAlgebra.Dual.Lemmas
    2import Mathlib.LinearAlgebra.Matrix.ToLin
    3
    4/-!
    5---
    6title: Paired-frame orbit under the primal and dual actions
    7type: theorem
    8---
    9Lemma 4.1: two individually injective pairs of frames with equal Gram
    10pairings differ by one ambient linear automorphism, acting contragrediently
    11on the dual frame. No nondegeneracy of the prescribed Gram is needed.
    12-/
    13
    14namespace Lax342547.PairedFrames
    15
    16universe u v w z
    17
    18variable {K : Type u} {U : Type v} {V : Type w} {W : Type z} [Field K]
    19 [AddCommGroup U] [Module K U]
    20 [AddCommGroup V] [Module K V] [hVdim : FiniteDimensional K V]
    21 [AddCommGroup W] [Module K W]
    22
    23axiom paired_frame_orbit {K : Type u} {U : Type v} {V : Type w} {W : Type z} [Field K]
    24 [AddCommGroup U] [Module K U]
    25 [AddCommGroup V] [Module K V] [FiniteDimensional K V]
    26 [AddCommGroup W] [Module K W]
    27 (A A' : U →ₗ[K] V) (B B' : W →ₗ[K] Module.Dual K V)
    28 (hA : Function.Injective A) (hA' : Function.Injective A')
    29 (hB : Function.Injective B) (hB' : Function.Injective B')
    30 (hgram : ∀ u w, B w (A u) = B' w (A' u)) :
    31 ∃ L : V ≃ₗ[K] V, (∀ u, L (A u) = A' u) ∧
    32 ∀ w v, B w (L.symm v) = B' w v
    33
    34axiom paired_matrix_orbit {I J N : Type} [Fintype I] [Fintype J] [Fintype N]
    35 [DecidableEq N] (A A' : Matrix N I K) (B B' : Matrix N J K)
    36 (hA : Function.Injective A.mulVec) (hA' : Function.Injective A'.mulVec)
    37 (hB : Function.Injective B.mulVec) (hB' : Function.Injective B'.mulVec)
    38 (hgram : A.transpose * B = A'.transpose * B') :
    39 ∃ C D : Matrix N N K, C * D = 1 ∧ D * C = 1 ∧
    40 C * A = A' ∧ D.transpose * B = B'
    41
    42end Lax342547.PairedFrames
    43
    Show ProofShow Proof
    Builds on

    none

    Used by
    From Mathlib

    Discussion

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

    Loading discussion…