NYLL
Module

FiniteTransgressionLinear.lean

Nyll.GaloisCohomology.ProP.FiniteTransgressionLinear
27 declarations indexed from sourceView source ↗

Module documentation

Linearity of finite transgression

Packages ambient-conjugation-invariant finite characters as a ZMod p-module and proves that the explicit finite transgression construction is linear. The kernel extension theorem then gives a criterion for linear independence of finite families of transgression classes.

Imports3
Imported by5

Declarations

instance

linearQuotientTopology

L31 ↗
ClassFieldTower.Cohomology.linearQuotientTopology
Source context 7 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {P : Type u} [Group P]
Lean source · statement
instance linearQuotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N)
instance

linearQuotientDiscrete

L32 ↗
ClassFieldTower.Cohomology.linearQuotientDiscrete
Source context 8 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {P : Type u} [Group P]
local instance linearQuotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N) := ⊥
Lean source · statement
instance linearQuotientDiscrete (N : Subgroup P) : DiscreteTopology (P ⧸ N)
abbrev

FiniteCharacter

L36 ↗
ClassFieldTower.Cohomology.FiniteCharacter
Documentation

Additive presentation of ZMod p-valued group characters.

Source context 9 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {P : Type u} [Group P]
local instance linearQuotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N) := ⊥
local instance linearQuotientDiscrete (N : Subgroup P) : DiscreteTopology (P ⧸ N) :=
  discreteTopology_bot _
Lean source · statement
abbrev FiniteCharacter (p : ℕ) (N : Type u) [Monoid N]
instance

finiteCharacterModule

L39 ↗
ClassFieldTower.Cohomology.finiteCharacterModule
Source context 9 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {P : Type u} [Group P]
local instance linearQuotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N) := ⊥
local instance linearQuotientDiscrete (N : Subgroup P) : DiscreteTopology (P ⧸ N) :=
  discreteTopology_bot _
Lean source · statement
instance finiteCharacterModule (N : Type u) [Monoid N] :
    Module (ZMod p) (FiniteCharacter p N)
def

invariantFiniteCharacterAddSubgroup

L48 ↗
ClassFieldTower.Cohomology.invariantFiniteCharacterAddSubgroup
Documentation

Ambient-conjugation-invariant finite characters, as an additive subgroup.

Source context 9 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {P : Type u} [Group P]
local instance linearQuotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N) := ⊥
local instance linearQuotientDiscrete (N : Subgroup P) : DiscreteTopology (P ⧸ N) :=
  discreteTopology_bot _
Lean source · full declaration
def invariantFiniteCharacterAddSubgroup (N : Subgroup P) [N.Normal] :
    AddSubgroup (FiniteCharacter p N) where
  carrier := {χ | ∀ (g : P) (n : N),
    χ.toMul (MulAut.conjNormal g n) = χ.toMul n}
  zero_mem' := by
    intro g n
    rfl
  add_mem' := by
    intro χ ψ hχ hψ g n
    change χ.toMul (MulAut.conjNormal g n) * ψ.toMul (MulAut.conjNormal g n) =
      χ.toMul n * ψ.toMul n
    rw [hχ g n, hψ g n]
  neg_mem' := by
    intro χ hχ g n
    change (χ.toMul (MulAut.conjNormal g n))⁻¹ = (χ.toMul n)⁻¹
    rw [hχ g n]
def

invariantFiniteCharacterSubmodule

L66 ↗
ClassFieldTower.Cohomology.invariantFiniteCharacterSubmodule
Documentation

Ambient-conjugation-invariant finite characters, as a ZMod p-module.

Source context 9 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {P : Type u} [Group P]
local instance linearQuotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N) := ⊥
local instance linearQuotientDiscrete (N : Subgroup P) : DiscreteTopology (P ⧸ N) :=
  discreteTopology_bot _
Lean source · statement
def invariantFiniteCharacterSubmodule (N : Subgroup P) [N.Normal] :
    Submodule (ZMod p) (FiniteCharacter p N)
abbrev

InvariantFiniteCharacter

L71 ↗
ClassFieldTower.Cohomology.InvariantFiniteCharacter
Documentation

An ambient-conjugation-invariant finite character.

Source context 9 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {P : Type u} [Group P]
local instance linearQuotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N) := ⊥
local instance linearQuotientDiscrete (N : Subgroup P) : DiscreteTopology (P ⧸ N) :=
  discreteTopology_bot _
Lean source · statement
abbrev InvariantFiniteCharacter (N : Subgroup P) [N.Normal]
def

toMonoidHom

L75 ↗
ClassFieldTower.Cohomology.InvariantFiniteCharacter.toMonoidHom
Documentation

The multiplicative presentation of an invariant finite character.

Source context 9 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {P : Type u} [Group P]
local instance linearQuotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N) := ⊥
local instance linearQuotientDiscrete (N : Subgroup P) : DiscreteTopology (P ⧸ N) :=
  discreteTopology_bot _
Lean source · statement
def InvariantFiniteCharacter.toMonoidHom (N : Subgroup P) [N.Normal]
    (χ : InvariantFiniteCharacter (p := p) N) :
    MonoidHom N (Multiplicative (ZMod p))
theorem

isInvariant

L80 ↗
ClassFieldTower.Cohomology.InvariantFiniteCharacter.isInvariant
Source context 9 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {P : Type u} [Group P]
local instance linearQuotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N) := ⊥
local instance linearQuotientDiscrete (N : Subgroup P) : DiscreteTopology (P ⧸ N) :=
  discreteTopology_bot _
Lean source · statement
theorem InvariantFiniteCharacter.isInvariant (N : Subgroup P) [N.Normal]
    (χ : InvariantFiniteCharacter (p := p) N) :
    ∀ (g : P) (n : N),
      InvariantFiniteCharacter.toMonoidHom N χ (MulAut.conjNormal g n) =
        InvariantFiniteCharacter.toMonoidHom N χ n
theorem

transgressionFactor_zero

L88 ↗
ClassFieldTower.Cohomology.transgressionFactor_zero
Source context 9 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {P : Type u} [Group P]
local instance linearQuotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N) := ⊥
local instance linearQuotientDiscrete (N : Subgroup P) : DiscreteTopology (P ⧸ N) :=
  discreteTopology_bot _
Lean source · statement
theorem transgressionFactor_zero (N : Subgroup P) [N.Normal]
    (q r : P ⧸ N) :
    transgressionFactor N
      ((0 : FiniteCharacter p N).toMul) q r = 0
theorem

transgressionFactor_add

L95 ↗
ClassFieldTower.Cohomology.transgressionFactor_add
Source context 9 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {P : Type u} [Group P]
local instance linearQuotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N) := ⊥
local instance linearQuotientDiscrete (N : Subgroup P) : DiscreteTopology (P ⧸ N) :=
  discreteTopology_bot _
Lean source · statement
theorem transgressionFactor_add (N : Subgroup P) [N.Normal]
    (χ ψ : FiniteCharacter p N) (q r : P ⧸ N) :
    transgressionFactor N ((χ + ψ).toMul) q r =
      transgressionFactor N χ.toMul q r +
        transgressionFactor N ψ.toMul q r
theorem

transgressionHomogeneousCochain_zero

L103 ↗
ClassFieldTower.Cohomology.transgressionHomogeneousCochain_zero
Source context 9 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {P : Type u} [Group P]
local instance linearQuotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N) := ⊥
local instance linearQuotientDiscrete (N : Subgroup P) : DiscreteTopology (P ⧸ N) :=
  discreteTopology_bot _
Lean source · statement
theorem transgressionHomogeneousCochain_zero (N : Subgroup P) [N.Normal] :
    transgressionHomogeneousCochain N
      ((0 : FiniteCharacter p N).toMul) = 0
theorem

transgressionHomogeneousCochain_add

L117 ↗
ClassFieldTower.Cohomology.transgressionHomogeneousCochain_add
Source context 9 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {P : Type u} [Group P]
local instance linearQuotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N) := ⊥
local instance linearQuotientDiscrete (N : Subgroup P) : DiscreteTopology (P ⧸ N) :=
  discreteTopology_bot _
Lean source · statement
theorem transgressionHomogeneousCochain_add (N : Subgroup P) [N.Normal]
    (χ ψ : FiniteCharacter p N) :
    transgressionHomogeneousCochain N ((χ + ψ).toMul) =
      transgressionHomogeneousCochain N χ.toMul +
        transgressionHomogeneousCochain N ψ.toMul
theorem

transgressionHomogeneousCocycle_zero

L135 ↗
ClassFieldTower.Cohomology.transgressionHomogeneousCocycle_zero
Source context 9 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {P : Type u} [Group P]
local instance linearQuotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N) := ⊥
local instance linearQuotientDiscrete (N : Subgroup P) : DiscreteTopology (P ⧸ N) :=
  discreteTopology_bot _
Lean source · statement
theorem transgressionHomogeneousCocycle_zero (N : Subgroup P) [N.Normal] :
    transgressionHomogeneousCocycle N
      (InvariantFiniteCharacter.toMonoidHom N
        (0 : InvariantFiniteCharacter (p := p) N))
      (InvariantFiniteCharacter.isInvariant N 0) = 0
theorem

transgressionHomogeneousCocycle_add

L149 ↗
ClassFieldTower.Cohomology.transgressionHomogeneousCocycle_add
Source context 9 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {P : Type u} [Group P]
local instance linearQuotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N) := ⊥
local instance linearQuotientDiscrete (N : Subgroup P) : DiscreteTopology (P ⧸ N) :=
  discreteTopology_bot _
Lean source · statement
theorem transgressionHomogeneousCocycle_add (N : Subgroup P) [N.Normal]
    (χ ψ : InvariantFiniteCharacter (p := p) N) :
    transgressionHomogeneousCocycle N
        (InvariantFiniteCharacter.toMonoidHom N (χ + ψ))
        (InvariantFiniteCharacter.isInvariant N (χ + ψ)) =
      transgressionHomogeneousCocycle N
          (InvariantFiniteCharacter.toMonoidHom N χ)
          (InvariantFiniteCharacter.isInvariant N χ) +
        transgressionHomogeneousCocycle N
          (InvariantFiniteCharacter.toMonoidHom N ψ)
          (InvariantFiniteCharacter.isInvariant N ψ)
theorem

finiteTransgressionClass_zero

L171 ↗
ClassFieldTower.Cohomology.finiteTransgressionClass_zero
Source context 9 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {P : Type u} [Group P]
local instance linearQuotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N) := ⊥
local instance linearQuotientDiscrete (N : Subgroup P) : DiscreteTopology (P ⧸ N) :=
  discreteTopology_bot _
Lean source · statement
theorem finiteTransgressionClass_zero (N : Subgroup P) [N.Normal] :
    finiteTransgressionClass N
      (InvariantFiniteCharacter.toMonoidHom N
        (0 : InvariantFiniteCharacter (p := p) N))
      (InvariantFiniteCharacter.isInvariant N 0) = 0
theorem

finiteTransgressionClass_add

L180 ↗
ClassFieldTower.Cohomology.finiteTransgressionClass_add
Source context 9 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {P : Type u} [Group P]
local instance linearQuotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N) := ⊥
local instance linearQuotientDiscrete (N : Subgroup P) : DiscreteTopology (P ⧸ N) :=
  discreteTopology_bot _
Lean source · statement
theorem finiteTransgressionClass_add (N : Subgroup P) [N.Normal]
    (χ ψ : InvariantFiniteCharacter (p := p) N) :
    finiteTransgressionClass N
        (InvariantFiniteCharacter.toMonoidHom N (χ + ψ))
        (InvariantFiniteCharacter.isInvariant N (χ + ψ)) =
      finiteTransgressionClass N
          (InvariantFiniteCharacter.toMonoidHom N χ)
          (InvariantFiniteCharacter.isInvariant N χ) +
        finiteTransgressionClass N
          (InvariantFiniteCharacter.toMonoidHom N ψ)
          (InvariantFiniteCharacter.isInvariant N ψ)
def

finiteTransgressionAddHom

L195 ↗
ClassFieldTower.Cohomology.finiteTransgressionAddHom
Documentation

Finite transgression as an additive homomorphism.

Source context 9 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {P : Type u} [Group P]
local instance linearQuotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N) := ⊥
local instance linearQuotientDiscrete (N : Subgroup P) : DiscreteTopology (P ⧸ N) :=
  discreteTopology_bot _
Lean source · full declaration
def finiteTransgressionAddHom (N : Subgroup P) [N.Normal] :
    InvariantFiniteCharacter (p := p) N →+
      continuousCohomologyZModPLifted p (P ⧸ N) 2 where
  toFun χ := finiteTransgressionClass N
    (InvariantFiniteCharacter.toMonoidHom N χ)
    (InvariantFiniteCharacter.isInvariant N χ)
  map_zero' := finiteTransgressionClass_zero N
  map_add' := finiteTransgressionClass_add N
def

finiteTransgressionLinearMap

L205 ↗
ClassFieldTower.Cohomology.finiteTransgressionLinearMap
Documentation

Finite transgression as a ZMod p-linear map.

Source context 9 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {P : Type u} [Group P]
local instance linearQuotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N) := ⊥
local instance linearQuotientDiscrete (N : Subgroup P) : DiscreteTopology (P ⧸ N) :=
  discreteTopology_bot _
Lean source · statement
def finiteTransgressionLinearMap (N : Subgroup P) [N.Normal] :
    InvariantFiniteCharacter (p := p) N →ₗ[ZMod p]
      continuousCohomologyZModPLifted p (P ⧸ N) 2
theorem

finiteTransgressionLinearMap_apply

L211 ↗
ClassFieldTower.Cohomology.finiteTransgressionLinearMap_apply
Source context 9 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {P : Type u} [Group P]
local instance linearQuotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N) := ⊥
local instance linearQuotientDiscrete (N : Subgroup P) : DiscreteTopology (P ⧸ N) :=
  discreteTopology_bot _
Lean source · statement
theorem finiteTransgressionLinearMap_apply (N : Subgroup P) [N.Normal]
    (χ : InvariantFiniteCharacter (p := p) N) :
    finiteTransgressionLinearMap N χ = finiteTransgressionClass N
      (InvariantFiniteCharacter.toMonoidHom N χ)
      (InvariantFiniteCharacter.isInvariant N χ)
theorem

finiteTransgressionLinearMap_zero

L219 ↗
ClassFieldTower.Cohomology.finiteTransgressionLinearMap_zero
Source context 9 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {P : Type u} [Group P]
local instance linearQuotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N) := ⊥
local instance linearQuotientDiscrete (N : Subgroup P) : DiscreteTopology (P ⧸ N) :=
  discreteTopology_bot _
Lean source · statement
theorem finiteTransgressionLinearMap_zero (N : Subgroup P) [N.Normal] :
    finiteTransgressionLinearMap N
      (0 : InvariantFiniteCharacter (p := p) N) = 0
theorem

finiteTransgressionLinearMap_add

L225 ↗
ClassFieldTower.Cohomology.finiteTransgressionLinearMap_add
Source context 9 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {P : Type u} [Group P]
local instance linearQuotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N) := ⊥
local instance linearQuotientDiscrete (N : Subgroup P) : DiscreteTopology (P ⧸ N) :=
  discreteTopology_bot _
Lean source · statement
theorem finiteTransgressionLinearMap_add (N : Subgroup P) [N.Normal]
    (χ ψ : InvariantFiniteCharacter (p := p) N) :
    finiteTransgressionLinearMap N (χ + ψ) =
      finiteTransgressionLinearMap N χ + finiteTransgressionLinearMap N ψ
theorem

finiteTransgressionLinearMap_smul

L232 ↗
ClassFieldTower.Cohomology.finiteTransgressionLinearMap_smul
Source context 9 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {P : Type u} [Group P]
local instance linearQuotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N) := ⊥
local instance linearQuotientDiscrete (N : Subgroup P) : DiscreteTopology (P ⧸ N) :=
  discreteTopology_bot _
Lean source · statement
theorem finiteTransgressionLinearMap_smul (N : Subgroup P) [N.Normal]
    (a : ZMod p) (χ : InvariantFiniteCharacter (p := p) N) :
    finiteTransgressionLinearMap N (a • χ) =
      a • finiteTransgressionLinearMap N χ
def

ExtendsToAmbient

L239 ↗
ClassFieldTower.Cohomology.InvariantFiniteCharacter.ExtendsToAmbient
Documentation

A character extends to the ambient group if it is the restriction of an ambient character.

Source context 9 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {P : Type u} [Group P]
local instance linearQuotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N) := ⊥
local instance linearQuotientDiscrete (N : Subgroup P) : DiscreteTopology (P ⧸ N) :=
  discreteTopology_bot _
Lean source · statement
def InvariantFiniteCharacter.ExtendsToAmbient (N : Subgroup P) [N.Normal]
    (χ : InvariantFiniteCharacter (p := p) N) : Prop
theorem

extendsToAmbient_of_transgression_eq_zero

L245 ↗
ClassFieldTower.Cohomology.InvariantFiniteCharacter.extendsToAmbient_of_transgression_eq_zero
Documentation

The kernel of finite transgression consists of extendable invariant characters.

Source context 9 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {P : Type u} [Group P]
local instance linearQuotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N) := ⊥
local instance linearQuotientDiscrete (N : Subgroup P) : DiscreteTopology (P ⧸ N) :=
  discreteTopology_bot _
Lean source · statement
theorem InvariantFiniteCharacter.extendsToAmbient_of_transgression_eq_zero
    (N : Subgroup P) [N.Normal]
    (χ : InvariantFiniteCharacter (p := p) N)
    (hχ : finiteTransgressionLinearMap N χ = 0) :
    InvariantFiniteCharacter.ExtendsToAmbient N χ
theorem

linearIndependent_finiteTransgressionLinearMap_of_no_extendableCombination

L257 ↗
ClassFieldTower.Cohomology.linearIndependent_finiteTransgressionLinearMap_of_no_extendableCombination
Documentation

A family has linearly independent transgression classes if no nonzero finite linear combination of its characters extends to the ambient group.

Source context 9 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {P : Type u} [Group P]
local instance linearQuotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N) := ⊥
local instance linearQuotientDiscrete (N : Subgroup P) : DiscreteTopology (P ⧸ N) :=
  discreteTopology_bot _
Lean source · full declaration
theorem linearIndependent_finiteTransgressionLinearMap_of_no_extendableCombination
    {ι : Type*} (N : Subgroup P) [N.Normal]
    (v : ι → InvariantFiniteCharacter (p := p) N)
    (hno : ∀ l : ι →₀ ZMod p,
      InvariantFiniteCharacter.ExtendsToAmbient N
        (Finsupp.linearCombination (ZMod p) v l) → l = 0) :
    LinearIndependent (ZMod p) (fun i ↦ finiteTransgressionLinearMap N (v i)) := by
  rw [linearIndependent_iff]
  intro l hl
  apply hno l
  apply InvariantFiniteCharacter.extendsToAmbient_of_transgression_eq_zero N
  rw [LinearMap.map_finsupp_linearCombination]
  exact hl
theorem

linearIndependent_finiteTransgressionClass_of_no_extendableCombination

L272 ↗
ClassFieldTower.Cohomology.linearIndependent_finiteTransgressionClass_of_no_extendableCombination
Documentation

The preceding criterion, stated directly for explicit finite transgression classes.

Source context 9 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {P : Type u} [Group P]
local instance linearQuotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N) := ⊥
local instance linearQuotientDiscrete (N : Subgroup P) : DiscreteTopology (P ⧸ N) :=
  discreteTopology_bot _
Lean source · full declaration
theorem linearIndependent_finiteTransgressionClass_of_no_extendableCombination
    {ι : Type*} (N : Subgroup P) [N.Normal]
    (v : ι → InvariantFiniteCharacter (p := p) N)
    (hno : ∀ l : ι →₀ ZMod p,
      InvariantFiniteCharacter.ExtendsToAmbient N
        (Finsupp.linearCombination (ZMod p) v l) → l = 0) :
    LinearIndependent (ZMod p) (fun i ↦ finiteTransgressionClass N
      (InvariantFiniteCharacter.toMonoidHom N (v i))
      (InvariantFiniteCharacter.isInvariant N (v i))) := by
  simpa only [finiteTransgressionLinearMap_apply] using
    linearIndependent_finiteTransgressionLinearMap_of_no_extendableCombination N v hno

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