NYLL
Module

FiniteStageTransgressionLinear.lean

Nyll.GaloisCohomology.ProP.FiniteStageTransgressionLinear
9 declarations indexed from sourceView source ↗

Module documentation

Linear finite-stage transgression

Defines finite-stage inflation as a linear map, composes it with the explicit finite transgression map, and transports the no-extendable-combination independence criterion across injective degree-two inflation.

Imports3
Imported by5

Declarations

instance

inflatedLinearStageTargetTopology

L32 ↗
ClassFieldTower.ProP.inflatedLinearStageTargetTopology
Source context 7 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups ProCGroups.ProC
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
Lean source · statement
instance inflatedLinearStageTargetTopology
    (R : ClosedSubgroup F)
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    TopologicalSpace
      ((F ⧸ (U.1 : Subgroup F)) ⧸ finiteStageImage R U)
instance

inflatedLinearStageTargetDiscrete

L38 ↗
ClassFieldTower.ProP.inflatedLinearStageTargetDiscrete
Source context 8 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups ProCGroups.ProC
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
local instance inflatedLinearStageTargetTopology
    (R : ClosedSubgroup F)
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    TopologicalSpace
      ((F ⧸ (U.1 : Subgroup F)) ⧸ finiteStageImage R U) := ⊥
Lean source · statement
instance inflatedLinearStageTargetDiscrete
    (R : ClosedSubgroup F)
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    DiscreteTopology
      ((F ⧸ (U.1 : Subgroup F)) ⧸ finiteStageImage R U)
def

finiteStageInflationLinearMap

L48 ↗
ClassFieldTower.ProP.finiteStageInflationLinearMap
Documentation

Inflation from the finite-stage quotient to the original quotient.

Source context 10 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups ProCGroups.ProC
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
local instance inflatedLinearStageTargetTopology
    (R : ClosedSubgroup F)
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    TopologicalSpace
      ((F ⧸ (U.1 : Subgroup F)) ⧸ finiteStageImage R U) := ⊥
local instance inflatedLinearStageTargetDiscrete
    (R : ClosedSubgroup F)
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    DiscreteTopology
      ((F ⧸ (U.1 : Subgroup F)) ⧸ finiteStageImage R U) :=
  discreteTopology_bot _
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
Lean source · statement
def finiteStageInflationLinearMap
    (R : ClosedSubgroup F) [R.Normal]
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    ClassFieldTower.Cohomology.continuousCohomologyZModPLifted p
        ((F ⧸ (U.1 : Subgroup F)) ⧸ finiteStageImage R U) 2 →ₗ[ZMod p]
      ClassFieldTower.Cohomology.continuousCohomologyZModPLifted p
        (F ⧸ (R : Subgroup F)) 2
def

inflatedFiniteTransgressionLinearMap

L59 ↗
ClassFieldTower.ProP.inflatedFiniteTransgressionLinearMap
Documentation

Finite transgression followed by inflation to H²(F/R, ZMod p).

Source context 10 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups ProCGroups.ProC
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
local instance inflatedLinearStageTargetTopology
    (R : ClosedSubgroup F)
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    TopologicalSpace
      ((F ⧸ (U.1 : Subgroup F)) ⧸ finiteStageImage R U) := ⊥
local instance inflatedLinearStageTargetDiscrete
    (R : ClosedSubgroup F)
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    DiscreteTopology
      ((F ⧸ (U.1 : Subgroup F)) ⧸ finiteStageImage R U) :=
  discreteTopology_bot _
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
Lean source · statement
def inflatedFiniteTransgressionLinearMap
    (R : ClosedSubgroup F) [R.Normal]
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    ClassFieldTower.Cohomology.InvariantFiniteCharacter (p := p)
        (finiteStageImage R U) →ₗ[ZMod p]
      ClassFieldTower.Cohomology.continuousCohomologyZModPLifted p
        (F ⧸ (R : Subgroup F)) 2
theorem

inflatedFiniteTransgressionLinearMap_apply

L72 ↗
ClassFieldTower.ProP.inflatedFiniteTransgressionLinearMap_apply
Source context 11 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups ProCGroups.ProC
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
local instance inflatedLinearStageTargetTopology
    (R : ClosedSubgroup F)
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    TopologicalSpace
      ((F ⧸ (U.1 : Subgroup F)) ⧸ finiteStageImage R U) := ⊥
local instance inflatedLinearStageTargetDiscrete
    (R : ClosedSubgroup F)
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    DiscreteTopology
      ((F ⧸ (U.1 : Subgroup F)) ⧸ finiteStageImage R U) :=
  discreteTopology_bot _
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
omit [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F] in
Lean source · statement
theorem inflatedFiniteTransgressionLinearMap_apply
    (R : ClosedSubgroup F) [R.Normal]
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F)
    (χ : ClassFieldTower.Cohomology.InvariantFiniteCharacter (p := p)
      (finiteStageImage R U)) :
    inflatedFiniteTransgressionLinearMap R U χ =
      inflatedFiniteTransgressionClass R U
        (ClassFieldTower.Cohomology.InvariantFiniteCharacter.toMonoidHom
          (finiteStageImage R U) χ)
        (ClassFieldTower.Cohomology.InvariantFiniteCharacter.isInvariant
          (finiteStageImage R U) χ)
theorem

inflatedFiniteTransgressionLinearMap_zero

L87 ↗
ClassFieldTower.ProP.inflatedFiniteTransgressionLinearMap_zero
Source context 11 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups ProCGroups.ProC
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
local instance inflatedLinearStageTargetTopology
    (R : ClosedSubgroup F)
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    TopologicalSpace
      ((F ⧸ (U.1 : Subgroup F)) ⧸ finiteStageImage R U) := ⊥
local instance inflatedLinearStageTargetDiscrete
    (R : ClosedSubgroup F)
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    DiscreteTopology
      ((F ⧸ (U.1 : Subgroup F)) ⧸ finiteStageImage R U) :=
  discreteTopology_bot _
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
omit [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F] in
Lean source · statement
theorem inflatedFiniteTransgressionLinearMap_zero
    (R : ClosedSubgroup F) [R.Normal]
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    inflatedFiniteTransgressionLinearMap R U
      (0 : ClassFieldTower.Cohomology.InvariantFiniteCharacter (p := p)
        (finiteStageImage R U)) = 0
theorem

inflatedFiniteTransgressionLinearMap_add

L97 ↗
ClassFieldTower.ProP.inflatedFiniteTransgressionLinearMap_add
Source context 11 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups ProCGroups.ProC
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
local instance inflatedLinearStageTargetTopology
    (R : ClosedSubgroup F)
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    TopologicalSpace
      ((F ⧸ (U.1 : Subgroup F)) ⧸ finiteStageImage R U) := ⊥
local instance inflatedLinearStageTargetDiscrete
    (R : ClosedSubgroup F)
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    DiscreteTopology
      ((F ⧸ (U.1 : Subgroup F)) ⧸ finiteStageImage R U) :=
  discreteTopology_bot _
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
omit [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F] in
Lean source · statement
theorem inflatedFiniteTransgressionLinearMap_add
    (R : ClosedSubgroup F) [R.Normal]
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F)
    (χ ψ : ClassFieldTower.Cohomology.InvariantFiniteCharacter (p := p)
      (finiteStageImage R U)) :
    inflatedFiniteTransgressionLinearMap R U (χ + ψ) =
      inflatedFiniteTransgressionLinearMap R U χ +
        inflatedFiniteTransgressionLinearMap R U ψ
theorem

inflatedFiniteTransgressionLinearMap_smul

L109 ↗
ClassFieldTower.ProP.inflatedFiniteTransgressionLinearMap_smul
Source context 11 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups ProCGroups.ProC
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
local instance inflatedLinearStageTargetTopology
    (R : ClosedSubgroup F)
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    TopologicalSpace
      ((F ⧸ (U.1 : Subgroup F)) ⧸ finiteStageImage R U) := ⊥
local instance inflatedLinearStageTargetDiscrete
    (R : ClosedSubgroup F)
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    DiscreteTopology
      ((F ⧸ (U.1 : Subgroup F)) ⧸ finiteStageImage R U) :=
  discreteTopology_bot _
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
omit [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F] in
Lean source · statement
theorem inflatedFiniteTransgressionLinearMap_smul
    (R : ClosedSubgroup F) [R.Normal]
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F)
    (a : ZMod p)
    (χ : ClassFieldTower.Cohomology.InvariantFiniteCharacter (p := p)
      (finiteStageImage R U)) :
    inflatedFiniteTransgressionLinearMap R U (a • χ) =
      a • inflatedFiniteTransgressionLinearMap R U χ
theorem

linearIndependent_inflatedFiniteTransgressionClass_of_injective

L122 ↗
ClassFieldTower.ProP.linearIndependent_inflatedFiniteTransgressionClass_of_injective
Documentation

Inflation preserves the finite-stage independence criterion when it is injective in degree two.

Source context 11 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups ProCGroups.ProC
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
local instance inflatedLinearStageTargetTopology
    (R : ClosedSubgroup F)
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    TopologicalSpace
      ((F ⧸ (U.1 : Subgroup F)) ⧸ finiteStageImage R U) := ⊥
local instance inflatedLinearStageTargetDiscrete
    (R : ClosedSubgroup F)
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    DiscreteTopology
      ((F ⧸ (U.1 : Subgroup F)) ⧸ finiteStageImage R U) :=
  discreteTopology_bot _
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
omit [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F] in
Lean source · full declaration
theorem linearIndependent_inflatedFiniteTransgressionClass_of_injective
    {ι : Type*}
    (R : ClosedSubgroup F) [R.Normal]
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F)
    (hinfl : Function.Injective (finiteStageInflationLinearMap R U))
    (v : ι → ClassFieldTower.Cohomology.InvariantFiniteCharacter (p := p)
      (finiteStageImage R U))
    (hno : ∀ l : ι →₀ ZMod p,
      ClassFieldTower.Cohomology.InvariantFiniteCharacter.ExtendsToAmbient
        (finiteStageImage R U)
        (Finsupp.linearCombination (ZMod p) v l) → l = 0) :
    LinearIndependent (ZMod p) (fun i ↦ inflatedFiniteTransgressionClass R U
      (ClassFieldTower.Cohomology.InvariantFiniteCharacter.toMonoidHom
        (finiteStageImage R U) (v i))
      (ClassFieldTower.Cohomology.InvariantFiniteCharacter.isInvariant
        (finiteStageImage R U) (v i))) := by
  have hbase :=
    (open _root_.ClassFieldTower.Cohomology in
      linearIndependent_finiteTransgressionLinearMap_of_no_extendableCombination
        (finiteStageImage R U) v hno)
  have himage := hbase.map' (finiteStageInflationLinearMap R U)
    (LinearMap.ker_eq_bot.mpr hinfl)
  change LinearIndependent (ZMod p)
    (fun i ↦ inflatedFiniteTransgressionLinearMap R U (v i)) at himage
  simpa only [inflatedFiniteTransgressionLinearMap_apply] using himage

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