Lax Lean Archive

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

The bundle lemma

Lax149335.BundleLemma · concepts/Lax149335/BundleLemma.lean · lax-149335

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

    Lemma 6.7 (Bundles). For every type AA, there are arbitrarily large numbers kk such that the concatenation map

    (Ak)∗×A<k↣A∗(A^k)^* \times A^{<k} \rightarrowtail A^*

    is an isomorphism. Here AiA^i is the ii-fold product of AA with itself, with A0=1A^0 = 1, and A<kA^{<k} is the co-product of all AiA^i with 0≤i<k0 \le i < k.

    Concept map
    6 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Lax149335.InjectiveSurjectiveTerms
    2
    3/-!
    4---
    5title: The bundle lemma
    6type: lemma
    7---
    8**Lemma 6.7 (Bundles).** For every type AA, there are arbitrarily large numbers kk such
    9that the concatenation map
    10
    11(Ak)∗×A<k↣A∗(A^k)^* \times A^{<k} \rightarrowtail A^*
    12
    13is an isomorphism. Here AiA^i is the ii-fold product of AA with itself, with
    14A0=1A^0 = 1, and A<kA^{<k} is the co-product of all AiA^i with 0≤i<k0 \le i < k.
    15
    16# Formalization notes
    17
    18The bundle size is written k+1k + 1, so that A<k+1=A0+⋯+AkA^{<k+1} = A^0 + \cdots + A^k is the type
    19constructor `TyF.lt k`. The formal statement is stronger than the paper's: the bundle
    20sizes k+1k + 1 can be chosen independently of the type AA.
    21-/
    22
    23namespace Lax149335.BundleLemma
    24
    25open Lax149335.Types Lax149335.Terms Lax149335.DerivedTerms Lax149335.DerivedTerms.Term
    26 Lax149335.InjectiveSurjectiveTerms
    27
    28/-- **Lemma 6.7.** For every `N` there is a `k ≥ N` such that, for every type `A`, the
    29concatenation map `(A^{k+1})* × A^{<k+1} ↣ A*` is an isomorphism. -/
    30axiom concatMap_bundle_iso_arbitrarily_large' (N : ℕ) :
    31 ∃ k : ℕ, N ≤ k ∧ ∀ A : Ty,
    32 ProvableIso (TyF.concatMap (.prod (.list (TyF.pow (k + 1))) (TyF.lt k)) A)
    33
    34end Lax149335.BundleLemma
    35
    Show Proof
    Formalization notes

    The bundle size is written k+1k + 1, so that A<k+1=A0+⋯+AkA^{<k+1} = A^0 + \cdots + A^k is the type constructor TyF.ltkTyF.lt k. The formal statement is stronger than the paper's: the bundle sizes k+1k + 1 can be chosen independently of the type AA.

    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

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

    Loading discussion…