Lax Lean Archive

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

Rank loss under restriction of a bilinear form

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

    Restricting both arguments to a subspace of codimension c loses at most 2c in rank. No symmetry, positivity, or characteristic assumption is needed. Applied to the polar form, this is the rank-loss step in the unary mixer estimate of Lemma 5.5.

    Concept map
    1 concept
    100%
    Proven claimThis conceptDescendants 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 bilinear_pullback_rank proven

    2 bilinear_restriction_rank proven

    Lean source view on GitHub

    1import Mathlib.LinearAlgebra.BilinearForm.Properties
    2import Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
    3
    4/-!
    5---
    6title: Rank loss under restriction of a bilinear form
    7type: theorem
    8---
    9Restricting both arguments to a subspace of codimension c loses at
    10most 2c in rank. No symmetry, positivity, or characteristic assumption
    11is needed. Applied to the polar form, this is the rank-loss step in
    12the unary mixer estimate of Lemma 5.5.
    13-/
    14
    15namespace Lax342547.RestrictionRank
    16
    17axiom bilinear_restriction_rank {K V : Type} [Field K] [AddCommGroup V] [Module K V]
    18 [FiniteDimensional K V] (B : LinearMap.BilinForm K V) (S : Submodule K V) :
    19 Module.finrank K (LinearMap.range B) ≤ Module.finrank K (LinearMap.range (B.restrict S)) +
    20 2 * (Module.finrank K V - Module.finrank K S)
    21
    22axiom bilinear_pullback_rank {K V W : Type} [Field K] [AddCommGroup V] [Module K V]
    23 [AddCommGroup W] [Module K W] [FiniteDimensional K V]
    24 (B : LinearMap.BilinForm K V) (A : W →ₗ[K] V) :
    25 Module.finrank K (LinearMap.range B) ≤ Module.finrank K (LinearMap.range (B.comp A A)) +
    26 2 * (Module.finrank K V - Module.finrank K (LinearMap.range A))
    27
    28end Lax342547.RestrictionRank
    29
    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…