NYLL
Module

TruncatedInequality.lean

Nyll.ProCGroups.GolodShafarevich.TruncatedInequality
6 declarations indexed from sourceView source ↗

Module documentation

Truncated Golod--Shafarevich dimension inequality

The numerical core is rank--nullity for a right-exact sequence of finite dimensional vector spaces. It is stated separately from the filtered Fox maps so the Nat arithmetic and the linear-algebra argument remain reusable.

Imports4
Imported by3

Declarations

theorem

finrank_add_le_of_linear_rightExact

L31 ↗
ClassFieldTower.ProP.finrank_add_le_of_linear_rightExact
Documentation

Dimension inequality attached to a right-exact sequence of finite dimensional vector spaces.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open ProCGroups
noncomputable section
universe u v₀ v₁ v₂ v₃
Lean source · statement
theorem finrank_add_le_of_linear_rightExact
    {k : Type u} [DivisionRing k]
    {R : Type v₀} {X : Type v₁} {Y : Type v₂} {Z : Type v₃}
    [AddCommGroup R] [Module k R] [FiniteDimensional k R]
    [AddCommGroup X] [Module k X] [FiniteDimensional k X]
    [AddCommGroup Y] [Module k Y] [FiniteDimensional k Y]
    [AddCommGroup Z] [Module k Z] [FiniteDimensional k Z]
    (f : R →ₗ[k] X) (g : X →ₗ[k] Y) (h : Y →ₗ[k] Z)
    (hfg : Function.Exact f g) (hgh : Function.Exact g h)
    (hh : Function.Surjective h) :
    Module.finrank k X + Module.finrank k Z ≤
      Module.finrank k Y + Module.finrank k R
instance

truncatedInequalityCanonicalZModAddCommGroup

L57 ↗
ClassFieldTower.ProP.truncatedInequalityCanonicalZModAddCommGroup
Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open ProCGroups
noncomputable section
universe u v₀ v₁ v₂ v₃
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]

-- Keep the self-module on `ZMod p` canonical when nilpotent-group instances are in scope.
Lean source · statement
instance truncatedInequalityCanonicalZModAddCommGroup : AddCommGroup (ZMod p)
instance

truncatedInequalityCanonicalZModModule

L59 ↗
ClassFieldTower.ProP.truncatedInequalityCanonicalZModModule
Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open ProCGroups
noncomputable section
universe u v₀ v₁ v₂ v₃
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]

-- Keep the self-module on `ZMod p` canonical when nilpotent-group instances are in scope.
local instance truncatedInequalityCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
Lean source · statement
instance truncatedInequalityCanonicalZModModule : Module (ZMod p) (ZMod p)
theorem

shiftedTruncation_coefficient_inequality_of_rightExact

L65 ↗
ClassFieldTower.ProP.shiftedTruncation_coefficient_inequality_of_rightExact
Documentation

Rank--nullity on shifted augmentation truncations, before inserting the concrete filtered Fox maps.

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open ProCGroups
noncomputable section
universe u v₀ v₁ v₂ v₃
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]

-- Keep the self-module on `ZMod p` canonical when nilpotent-group instances are in scope.
local instance truncatedInequalityCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance truncatedInequalityCanonicalZModModule : Module (ZMod p) (ZMod p) :=
  Semiring.toModule
omit [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in
Lean source · statement
theorem shiftedTruncation_coefficient_inequality_of_rightExact
    [Finite G] {d r N : ℕ} (ν : Fin r → ℕ)
    (f : (∀ i : Fin r,
        ShiftedAugmentationTruncation (p := p) (G := G) N (ν i)) →ₗ[ZMod p]
      (Fin d → ShiftedAugmentationTruncation (p := p) (G := G) N 1))
    (g : (Fin d → ShiftedAugmentationTruncation (p := p) (G := G) N 1) →ₗ[ZMod p]
      ShiftedAugmentationTruncation (p := p) (G := G) N 0)
    (h : ShiftedAugmentationTruncation (p := p) (G := G) N 0 →ₗ[ZMod p]
      ZMod p)
    (hfg : Function.Exact f g) (hgh : Function.Exact g h)
    (hh : Function.Surjective h) :
    1 + d * shiftedTruncatedAugmentationDimension (p := p) (G := G) N 1 ≤
      truncatedAugmentationDimension (p := p) (G := G) N +
        ∑ i, shiftedTruncatedAugmentationDimension (p := p) (G := G) N (ν i)
theorem

natSafe_truncatedAugmentationCoefficientInequality_of_rightExact

L99 ↗
ClassFieldTower.ProP.natSafe_truncatedAugmentationCoefficientInequality_of_rightExact
Documentation

Nat-safe form of the truncated coefficient inequality.

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open ProCGroups
noncomputable section
universe u v₀ v₁ v₂ v₃
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]

-- Keep the self-module on `ZMod p` canonical when nilpotent-group instances are in scope.
local instance truncatedInequalityCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance truncatedInequalityCanonicalZModModule : Module (ZMod p) (ZMod p) :=
  Semiring.toModule
omit [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in
Lean source · statement
theorem natSafe_truncatedAugmentationCoefficientInequality_of_rightExact
    [Finite G] {d r N : ℕ} (ν : Fin r → ℕ)
    (f : (∀ i : Fin r,
        ShiftedAugmentationTruncation (p := p) (G := G) N (ν i)) →ₗ[ZMod p]
      (Fin d → ShiftedAugmentationTruncation (p := p) (G := G) N 1))
    (g : (Fin d → ShiftedAugmentationTruncation (p := p) (G := G) N 1) →ₗ[ZMod p]
      ShiftedAugmentationTruncation (p := p) (G := G) N 0)
    (h : ShiftedAugmentationTruncation (p := p) (G := G) N 0 →ₗ[ZMod p]
      ZMod p)
    (hfg : Function.Exact f g) (hgh : Function.Exact g h)
    (hh : Function.Surjective h) :
    1 + d * truncatedAugmentationDimensionStar (p := p) (G := G) N 1 ≤
      truncatedAugmentationDimension (p := p) (G := G) N +
        ∑ i, truncatedAugmentationDimensionStar (p := p) (G := G) N (ν i)
theorem

finitePresentation_truncatedCoefficientInequality

L125 ↗
ClassFieldTower.ProP.finitePresentation_truncatedCoefficientInequality
Documentation

The Nat-safe truncated Golod--Shafarevich coefficient inequality attached to an actual finite pro-p presentation. All exactness inputs are supplied by the filtered Fox--Crowell sequence.

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open ProCGroups
noncomputable section
universe u v₀ v₁ v₂ v₃
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]

-- Keep the self-module on `ZMod p` canonical when nilpotent-group instances are in scope.
local instance truncatedInequalityCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance truncatedInequalityCanonicalZModModule : Module (ZMod p) (ZMod p) :=
  Semiring.toModule
variable {d r : ℕ}
variable {sourceData :
  FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
    (FiniteGroupClass.pGroup p)}
Lean source · statement
theorem finitePresentation_truncatedCoefficientInequality
    [Finite G]
    (P : FiniteProPPresentation p d r sourceData G)
    (ν : Fin r → ℕ)
    (hν : ∀ j, P.RelatorZassenhausDepthAtLeast (ν j) j)
    (N : ℕ) :
    1 + d * truncatedAugmentationDimensionStar (p := p) (G := G) N 1 ≤
      truncatedAugmentationDimension (p := p) (G := G) N +
        ∑ i, truncatedAugmentationDimensionStar
          (p := p) (G := G) N (ν i)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.