NYLL
Module

TorsorCharacter.lean

Nyll.EtaleFundamentalGroups.Cohomology.TorsorCharacter
6 declarations indexed from sourceView source ↗

Module documentation

Characters obtained from monodromy on abelian torsors

A continuous action on a discrete abelian torsor, commuting with translation, determines a continuous character. Its value is displacement of any chosen point; commutativity makes the answer independent of that point. This is the group-theoretic part of the degree-one étale cohomology comparison.

Imports4
Imported by7

Declarations

def

torsorCharacter

L33 ↗
EtaleFundamentalGroups.Cohomology.torsorCharacter
Documentation

Monodromy displacement in a discrete abelian torsor is a continuous character.

Source context 4 commands

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

noncomputable section
universe u v w
namespace EtaleFundamentalGroups.Cohomology
variable {G : Type u} [Group G] [TopologicalSpace G]
  {A : Type v} [CommGroup A] [TopologicalSpace A]
  {P : Type w} [Torsor A P] [MulAction G P] [SMulCommClass G A P]
  [TopologicalSpace P] [DiscreteTopology P] [ContinuousSMul G P]
Lean source · full declaration
def torsorCharacter (p : P) : G →ₜ* A where
  toFun g := (g • p) /ₛ p
  map_one' := by rw [one_smul, sdiv_self]
  map_mul' g h := by
    conv_lhs =>
      rw [mul_smul, ← sdiv_smul (h • p) p, smul_comm, smul_sdiv_assoc]
    exact mul_comm _ _
  continuous_toFun :=
    (continuous_of_discreteTopology : Continuous (fun q : P => q /ₛ p)).comp
      (continuous_id.smul continuous_const)
theorem

torsorCharacter_eq

L45 ↗
EtaleFundamentalGroups.Cohomology.torsorCharacter_eq
Documentation

For abelian coefficients the character is independent of the point in the torsor.

Source context 4 commands

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

noncomputable section
universe u v w
namespace EtaleFundamentalGroups.Cohomology
variable {G : Type u} [Group G] [TopologicalSpace G]
  {A : Type v} [CommGroup A] [TopologicalSpace A]
  {P : Type w} [Torsor A P] [MulAction G P] [SMulCommClass G A P]
  [TopologicalSpace P] [DiscreteTopology P] [ContinuousSMul G P]
Lean source · statement
theorem torsorCharacter_eq (p q : P) : torsorCharacter (G := G) p = torsorCharacter q
theorem

torsorCharacter_eq_one_iff

L53 ↗
EtaleFundamentalGroups.Cohomology.torsorCharacter_eq_one_iff
Documentation

The character is trivial exactly when one, equivalently every, point is fixed.

Source context 4 commands

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

noncomputable section
universe u v w
namespace EtaleFundamentalGroups.Cohomology
variable {G : Type u} [Group G] [TopologicalSpace G]
  {A : Type v} [CommGroup A] [TopologicalSpace A]
  {P : Type w} [Torsor A P] [MulAction G P] [SMulCommClass G A P]
  [TopologicalSpace P] [DiscreteTopology P] [ContinuousSMul G P]
Lean source · statement
theorem torsorCharacter_eq_one_iff (p : P) :
    torsorCharacter (G := G) p = 1 ↔ ∀ g : G, g • p = p
theorem

torsorCharacter_map

L67 ↗
EtaleFundamentalGroups.Cohomology.torsorCharacter_map
Documentation

An equivariant map preserving coefficient translations preserves the displacement character. No choice of torsor point enters this compatibility.

Source context 4 commands

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

noncomputable section
universe u v w
namespace EtaleFundamentalGroups.Cohomology
variable {G : Type u} [Group G] [TopologicalSpace G]
  {A : Type v} [CommGroup A] [TopologicalSpace A]
  {P : Type w} [Torsor A P] [MulAction G P] [SMulCommClass G A P]
  [TopologicalSpace P] [DiscreteTopology P] [ContinuousSMul G P]
Lean source · statement
theorem torsorCharacter_map
    {Q : Type*} [Torsor A Q] [MulAction G Q] [SMulCommClass G A Q]
    [TopologicalSpace Q] [DiscreteTopology Q] [ContinuousSMul G Q]
    (f : P → Q) (hf : ∀ a : A, ∀ p : P, f (a • p) = a • f p)
    (hg : ∀ g : G, ∀ p : P, f (g • p) = g • f p) (p : P) :
    torsorCharacter (G := G) p = torsorCharacter (f p)
def

torsorAbelianCharacter

L84 ↗
EtaleFundamentalGroups.Cohomology.torsorAbelianCharacter
Documentation

The character on the topological abelianization uses the actual quotient by the closed commutator subgroup.

Source context 4 commands

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

noncomputable section
universe u v w
namespace EtaleFundamentalGroups.Cohomology
variable {G : Type u} [Group G] [TopologicalSpace G]
  {A : Type v} [CommGroup A] [TopologicalSpace A]
  {P : Type w} [Torsor A P] [MulAction G P] [SMulCommClass G A P]
  [TopologicalSpace P] [DiscreteTopology P] [ContinuousSMul G P]
Lean source · statement
def torsorAbelianCharacter [IsTopologicalGroup G] [T1Space A] (p : P) :
    TopologicalAbelianization G →ₜ* A
theorem

torsorAbelianCharacter_apply_mk

L90 ↗
EtaleFundamentalGroups.Cohomology.torsorAbelianCharacter_apply_mk
Documentation

Evaluating the descended character on a quotient class gives the original monodromy displacement.

Source context 4 commands

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

noncomputable section
universe u v w
namespace EtaleFundamentalGroups.Cohomology
variable {G : Type u} [Group G] [TopologicalSpace G]
  {A : Type v} [CommGroup A] [TopologicalSpace A]
  {P : Type w} [Torsor A P] [MulAction G P] [SMulCommClass G A P]
  [TopologicalSpace P] [DiscreteTopology P] [ContinuousSMul G P]
Lean source · statement
theorem torsorAbelianCharacter_apply_mk [IsTopologicalGroup G] [T1Space A]
    (p : P) (g : G) :
    torsorAbelianCharacter p (ProCGroups.Abelian.TopologicalAbelianization.mk G g) =
      (g • p) /ₛ p

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