Documentation

LeanPool.MarkoffModP.BGS.HasseWeil.CechRiemannLinearAlgebra

The linear-algebra inequality in the Cech proof of Riemann's inequality #

Let A ≤ A' and B be subspaces of a vector space V. The canonical map

A' / A → V / (A ⊔ B)

has kernel canonically represented by

(A' ⊓ B) / (A ⊓ B).

Rank--nullity therefore gives

finrank (A' / A) ≤ finrank ((A' ⊓ B) / (A ⊓ B)) + finrank (V / (A ⊔ B)).

Only the three quotient spaces occurring in this argument need to be finite-dimensional; the ambient space V and the subspaces themselves may be infinite-dimensional. This is the abstract finite-dimensional step used by the Cech proof of Riemann's inequality.

source
@[reducible, inline]
abbrev BGS.HasseWeil.relativeSubmodule {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (A A' : Submodule K V) :
Submodule K ↥A'

The copy of A inside A'. When A ≤ A', this is the denominator in the relative quotient A' / A.

Equations
Instances For
    source
    def BGS.HasseWeil.cechRelativeQuotientMap {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (A A' B : Submodule K V) :
    ↥A' ⧸ relativeSubmodule A A' →ₗ[K] V ⧸ A ⊔ B

    The canonical map A' / A → V / (A ⊔ B) used in the Cech argument.

    Equations
    Instances For
      source
      def BGS.HasseWeil.cechIntersectionQuotientMap {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (A A' B : Submodule K V) :
      ↥(A' ⊓ B) ⧸ Submodule.comap (A' ⊓ B).subtype (A ⊓ B) →ₗ[K] ↥A' ⧸ relativeSubmodule A A'

      The quotient (A' ⊓ B) / (A ⊓ B) maps naturally into A' / A.

      Equations
      Instances For
        source
        theorem BGS.HasseWeil.cechIntersectionQuotientMap_injective {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (A A' B : Submodule K V) :
        Function.Injective ⇑(cechIntersectionQuotientMap A A' B)
        source
        theorem BGS.HasseWeil.range_cechIntersectionQuotientMap_eq_ker {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (A A' B : Submodule K V) (hAA' : A ≤ A') :
        (cechIntersectionQuotientMap A A' B).range = (cechRelativeQuotientMap A A' B).ker

        The intersection quotient identifies exactly with the kernel of the Cech relative quotient map.

        source
        theorem BGS.HasseWeil.finrank_relativeQuotient_eq_infQuotient_add_range {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (A A' B : Submodule K V) (hAA' : A ≤ A') [Module.Finite K (↥A' ⧸ relativeSubmodule A A')] :
        Module.finrank K (↥A' ⧸ relativeSubmodule A A') = Module.finrank K (↥(A' ⊓ B) ⧸ Submodule.comap (A' ⊓ B).subtype (A ⊓ B)) + Module.finrank K ↥(cechRelativeQuotientMap A A' B).range

        Rank--nullity with the Cech kernel written as the intersection quotient. This equality is the strongest finite-dimensional form of the abstract linear-algebra argument.

        source
        theorem BGS.HasseWeil.finrank_relativeQuotient_le_infQuotient_add_supQuotient {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (A A' B : Submodule K V) (hAA' : A ≤ A') [Module.Finite K (↥A' ⧸ relativeSubmodule A A')] [Module.Finite K (V ⧸ A ⊔ B)] :
        Module.finrank K (↥A' ⧸ relativeSubmodule A A') ≤ Module.finrank K (↥(A' ⊓ B) ⧸ Submodule.comap (A' ⊓ B).subtype (A ⊓ B)) + Module.finrank K (V ⧸ A ⊔ B)

        The abstract finite-dimensional inequality behind the Cech proof of Riemann's inequality. No finite-dimensionality hypothesis is imposed on the ambient vector space.

        source
        theorem BGS.HasseWeil.finrank_relativeQuotient_sub_supQuotient_le_infQuotient {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (A A' B : Submodule K V) (hAA' : A ≤ A') [Module.Finite K (↥A' ⧸ relativeSubmodule A A')] [Module.Finite K (V ⧸ A ⊔ B)] :
        Module.finrank K (↥A' ⧸ relativeSubmodule A A') - Module.finrank K (V ⧸ A ⊔ B) ≤ Module.finrank K (↥(A' ⊓ B) ⧸ Submodule.comap (A' ⊓ B).subtype (A ⊓ B))

        Subtractive form of finrank_relativeQuotient_le_infQuotient_add_supQuotient, convenient when the intersection quotient is the desired lower bound.