NYLL
Module

TorsorCharacterNaturality.lean

Nyll.EtaleFundamentalGroups.Cohomology.TorsorCharacterNaturality
2 declarations indexed from sourceView source ↗

Module documentation

Change of coefficients for torsor displacement characters

An equivariant map of torsors compatible with a coefficient homomorphism carries displacement to the image displacement. This is the group-theoretic naturality needed to prove additivity of the étale H¹ comparison.

Imports1
Imported by2

Declarations

abbrev

discreteCoefficientHom

L25 ↗
EtaleFundamentalGroups.Cohomology.discreteCoefficientHom
Documentation

An additive coefficient homomorphism, viewed as a continuous homomorphism between the associated discrete multiplicative groups.

Source context 3 commands

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

noncomputable section
universe u v w
namespace EtaleFundamentalGroups.Cohomology
Lean source · full declaration
abbrev discreteCoefficientHom {A : Type v} {B : Type w}
    [AddCommGroup A] [AddCommGroup B] (α : A →+ B) :
    let : TopologicalSpace (Multiplicative A) := ⊥
    let : TopologicalSpace (Multiplicative B) := ⊥
    Multiplicative A →ₜ* Multiplicative B := by
  let : TopologicalSpace (Multiplicative A) := ⊥
  let : TopologicalSpace (Multiplicative B) := ⊥
  have : DiscreteTopology (Multiplicative A) := ⟨rfl⟩
  exact ⟨α.toMultiplicative, continuous_of_discreteTopology⟩
theorem

torsorCharacter_comp

L37 ↗
EtaleFundamentalGroups.Cohomology.torsorCharacter_comp
Documentation

Displacement commutes with a change of coefficients when the actual torsor map preserves both actions. No bijectivity of that map is required.

Source context 3 commands

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

noncomputable section
universe u v w
namespace EtaleFundamentalGroups.Cohomology
Lean source · statement
theorem torsorCharacter_comp
    {G : Type u} [Group G] [TopologicalSpace G]
    {A : Type v} [CommGroup A] [TopologicalSpace A]
    {B : Type w} [CommGroup B] [TopologicalSpace B]
    {P Q : Type*} [Torsor A P] [Torsor B Q]
    [MulAction G P] [SMulCommClass G A P]
    [MulAction G Q] [SMulCommClass G B Q]
    [TopologicalSpace P] [DiscreteTopology P] [ContinuousSMul G P]
    [TopologicalSpace Q] [DiscreteTopology Q] [ContinuousSMul G Q]
    (α : A →ₜ* B) (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) :
    α.comp (torsorCharacter (G := G) p) = torsorCharacter (f p)

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