Lax Lean Archive

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

Actual factor lifts and covered offsets

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

    Common minimal quotient factors lift to actual endpoint factors, with covered differences, independent companion spaces, and the precise offset dimension budget.

    Concept map
    9 concepts; 1 descendant hidden
    100%
    Proven claimThis conceptRelated conceptA → B: B builds on A
    Evidence

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

    1 column_difference_in_cover proven

    2 common_quotient_offsets proven

    3 factor_difference_identity proven

    4 lift_common_factor proven

    5 lift_quotient_factor proven

    6 lifted_column_avoids_cover proven

    7 lifted_row_avoids_cover proven

    8 offset_dimension_budget proven

    9 restriction_range_of_avoidance proven

    10 row_difference_in_cover proven

    Lean source view on GitHub

    1import Lax342547.CoverAvoidance
    2import Mathlib.LinearAlgebra.Basis.VectorSpace
    3
    4/-!
    5---
    6title: Actual factor lifts and covered offsets
    7type: lemma
    8---
    9Common minimal quotient factors lift to actual endpoint factors, with covered differences, independent companion spaces, and the precise offset dimension budget.
    10-/
    11
    12namespace Lax342547.QuotientFactorLifts
    13
    14
    15
    16axiom lift_common_factor {K D U V W X : Type} [Field K]
    17 [AddCommGroup D] [Module K D] [AddCommGroup U] [Module K U]
    18 [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W]
    19 [AddCommGroup X] [Module K X]
    20 (π : W →ₗ[K] X) (C : U →ₗ[K] X) (M : V →ₗ[K] W)
    21 (B : D →ₗ[K] V) (R : D →ₗ[K] U)
    22 (hC : Function.Injective C) (hR : Function.Surjective R)
    23 (hπ : Disjoint (LinearMap.range M) (LinearMap.ker π))
    24 (hrange : LinearMap.range (M.comp B) = LinearMap.range M)
    25 (hcommon : π.comp (M.comp B) = C.comp R) :
    26 ∃ P : U →ₗ[K] W, ∃ Q : V →ₗ[K] U,
    27 P.comp Q = M ∧ π.comp P = C ∧ Q.comp B = R
    28
    29axiom restriction_range_of_avoidance {K V W : Type} [Field K]
    30 [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W]
    31 [FiniteDimensional K V] [FiniteDimensional K W]
    32 (M : V →ₗ[K] W) (T : Submodule K (Module.Dual K V))
    33 (hT : Disjoint (LinearMap.range M.dualMap) T) :
    34 LinearMap.range (M.comp T.dualCoannihilator.subtype) = LinearMap.range M
    35
    36axiom lift_quotient_factor {K U V W : Type} [Field K]
    37 [AddCommGroup U] [Module K U] [AddCommGroup V] [Module K V]
    38 [AddCommGroup W] [Module K W] [FiniteDimensional K V] [FiniteDimensional K W]
    39 (S : Submodule K W) (T : Submodule K (Module.Dual K V))
    40 (C : U →ₗ[K] (W ⧸ S)) (M : V →ₗ[K] W) (R : T.dualCoannihilator →ₗ[K] U)
    41 (hC : Function.Injective C) (hR : Function.Surjective R)
    42 (hS : Disjoint (LinearMap.range M) S) (hT : Disjoint (LinearMap.range M.dualMap) T)
    43 (hfactor : Lax342547.CoverProjection.projection M S T = C.comp R) :
    44 ∃ P : U →ₗ[K] W, ∃ Q : V →ₗ[K] U,
    45 P.comp Q = M ∧ S.mkQ.comp P = C ∧ Q.comp T.dualCoannihilator.subtype = R
    46
    47axiom column_difference_in_cover {K U W : Type} [Field K]
    48 [AddCommGroup U] [Module K U] [AddCommGroup W] [Module K W]
    49 (S : Submodule K W) (C : U →ₗ[K] (W ⧸ S)) (P₁ P₂ : U →ₗ[K] W)
    50 (h₁ : S.mkQ.comp P₁ = C) (h₂ : S.mkQ.comp P₂ = C) :
    51 LinearMap.range (P₁-P₂) ≤ S
    52
    53axiom row_difference_in_cover {K U V : Type} [Field K]
    54 [AddCommGroup U] [Module K U] [AddCommGroup V] [Module K V]
    55 [FiniteDimensional K V]
    56 (T : Submodule K (Module.Dual K V)) (R : T.dualCoannihilator →ₗ[K] U)
    57 (Q₁ Q₂ : V →ₗ[K] U)
    58 (h₁ : Q₁.comp T.dualCoannihilator.subtype = R)
    59 (h₂ : Q₂.comp T.dualCoannihilator.subtype = R) :
    60 LinearMap.range (Q₁-Q₂).dualMap ≤ T
    61
    62axiom factor_difference_identity {K U V W : Type} [Field K]
    63 [AddCommGroup U] [Module K U] [AddCommGroup V] [Module K V]
    64 [AddCommGroup W] [Module K W]
    65 (P₁ P₂ : U →ₗ[K] W) (Q₁ Q₂ : V →ₗ[K] U) :
    66 P₁.comp Q₁-P₂.comp Q₂ = (P₁-P₂).comp Q₂+P₁.comp (Q₁-Q₂)
    67
    68axiom lifted_column_avoids_cover {K U W : Type} [Field K]
    69 [AddCommGroup U] [Module K U] [AddCommGroup W] [Module K W]
    70 (S : Submodule K W) (C : U →ₗ[K] (W ⧸ S)) (P : U →ₗ[K] W)
    71 (hC : Function.Injective C) (hP : S.mkQ.comp P = C) :
    72 Disjoint (LinearMap.range P) S
    73
    74axiom offset_dimension_budget {K U V W : Type} [Field K]
    75 [AddCommGroup U] [Module K U] [AddCommGroup V] [Module K V]
    76 [AddCommGroup W] [Module K W] [FiniteDimensional K U]
    77 (P : U →ₗ[K] W) (Q : V →ₗ[K] U) :
    78 Module.finrank K (LinearMap.range P)+Module.finrank K (LinearMap.range Q.dualMap) ≤
    79 2*Module.finrank K U
    80
    81axiom lifted_row_avoids_cover {K U V : Type} [Field K]
    82 [AddCommGroup U] [Module K U] [AddCommGroup V] [Module K V]
    83 (T : Submodule K (Module.Dual K V)) (R : T.dualCoannihilator →ₗ[K] U)
    84 (Q : V →ₗ[K] U) (hR : Function.Surjective R)
    85 (hQ : Q.comp T.dualCoannihilator.subtype = R) :
    86 Disjoint (LinearMap.range Q.dualMap) T
    87
    88axiom common_quotient_offsets {K U V W : Type} [Field K]
    89 [AddCommGroup U] [Module K U] [AddCommGroup V] [Module K V]
    90 [AddCommGroup W] [Module K W] [FiniteDimensional K U]
    91 [FiniteDimensional K V] [FiniteDimensional K W]
    92 (S : Submodule K W) (T : Submodule K (Module.Dual K V))
    93 (C : U →ₗ[K] (W ⧸ S)) (R : T.dualCoannihilator →ₗ[K] U)
    94 (M₁ M₂ : V →ₗ[K] W) (hC : Function.Injective C) (hR : Function.Surjective R)
    95 (hS₁ : Disjoint (LinearMap.range M₁) S) (hT₁ : Disjoint (LinearMap.range M₁.dualMap) T)
    96 (hS₂ : Disjoint (LinearMap.range M₂) S) (hT₂ : Disjoint (LinearMap.range M₂.dualMap) T)
    97 (h₁ : Lax342547.CoverProjection.projection M₁ S T = C.comp R)
    98 (h₂ : Lax342547.CoverProjection.projection M₂ S T = C.comp R) :
    99 ∃ P₁ P₂ : U →ₗ[K] W, ∃ Q₁ Q₂ : V →ₗ[K] U,
    100 P₁.comp Q₁ = M₁ ∧ P₂.comp Q₂ = M₂ ∧
    101 LinearMap.range (P₁-P₂) ≤ S ∧ LinearMap.range (Q₁-Q₂).dualMap ≤ T ∧
    102 Disjoint (LinearMap.range P₁) S ∧ Disjoint (LinearMap.range Q₂.dualMap) T ∧
    103 M₁-M₂ = (P₁-P₂).comp Q₂+P₁.comp (Q₁-Q₂) ∧
    104 Module.finrank K (LinearMap.range (P₁-P₂))+
    105 Module.finrank K (LinearMap.range (Q₁-Q₂).dualMap) ≤ 2*Module.finrank K U
    106
    107end Lax342547.QuotientFactorLifts
    108
    Show ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow 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…