NYLL
Module

FiniteCharacterExtension.lean

Nyll.EtaleFundamentalGroups.Cohomology.FiniteCharacterExtension
5 declarations indexed from sourceView source ↗

Module documentation

A finite linear extension constructed from a character

For an additive abelian group A, a character acts on A × End(A) by g • (a, f) = (a + f(χ(g)), f). Thus both the kernel A and the quotient End(A) have trivial action. The inverse image of the identity endomorphism has displacement exactly χ. If A is finite, this whole extension is finite; no choice of an exponent or an invertibility hypothesis is required.

Imports5
  • Mathlib.Topology.Algebra.ContinuousMonoidHom
  • Mathlib.Topology.Algebra.MulAction
  • Mathlib.Algebra.Group.Hom.Instances
  • Mathlib.Algebra.Group.Prod
  • Mathlib.Algebra.Group.TypeTags.Hom
Imported by2

Declarations

abbrev

characterExtensionAction

L34 ↗
EtaleFundamentalGroups.Cohomology.characterExtensionAction
Documentation

The triangular action constructed from a continuous character.

Source context 4 commands

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

noncomputable section
universe u v
namespace EtaleFundamentalGroups.Cohomology
variable {G : Type v} [Group G] [TopologicalSpace G]
  {A : Type u} [AddCommGroup A] [TopologicalSpace A]
  (χ : G →ₜ* Multiplicative A)
Lean source · full declaration
abbrev characterExtensionAction : DistribMulAction G (A × (A →+ A)) where
  smul g x := (x.1 + x.2 (χ g).toAdd, x.2)
  one_smul x := by
    apply Prod.ext
    · change x.1 + x.2 (χ 1).toAdd = x.1
      rw [map_one]
      exact (congrArg (x.1 + ·) x.2.map_zero).trans (add_zero x.1)
    · rfl
  mul_smul g h x := by
    apply Prod.ext
    · change x.1 + x.2 (χ (g * h)).toAdd =
        (x.1 + x.2 (χ h).toAdd) + x.2 (χ g).toAdd
      rw [map_mul]
      change x.1 + x.2 ((χ g).toAdd + (χ h).toAdd) = _
      rw [map_add, add_comm (x.2 (χ g).toAdd), add_assoc]
    · rfl
  smul_zero g := by
    apply Prod.ext
    · exact add_zero 0
    · rfl
  smul_add g x y := by
    apply Prod.ext
    · change (x.1 + y.1) + (x.2 (χ g).toAdd + y.2 (χ g).toAdd) =
        (x.1 + x.2 (χ g).toAdd) + (y.1 + y.2 (χ g).toAdd)
      exact add_add_add_comm _ _ _ _
    · rfl
theorem

characterExtensionAction_continuous

L62 ↗
EtaleFundamentalGroups.Cohomology.characterExtensionAction_continuous
Documentation

The triangular action is continuous on the discrete extension group.

Source context 4 commands

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

noncomputable section
universe u v
namespace EtaleFundamentalGroups.Cohomology
variable {G : Type v} [Group G] [TopologicalSpace G]
  {A : Type u} [AddCommGroup A] [TopologicalSpace A]
  (χ : G →ₜ* Multiplicative A)
Lean source · full declaration
theorem characterExtensionAction_continuous [DiscreteTopology A] :
    let : TopologicalSpace (A × (A →+ A)) := ⊥
    let : DistribMulAction G (A × (A →+ A)) := characterExtensionAction χ
    ContinuousSMul G (A × (A →+ A)) := by
  let : TopologicalSpace (A × (A →+ A)) := ⊥
  have : DiscreteTopology (A × (A →+ A)) := ⟨rfl⟩
  let : DistribMulAction G (A × (A →+ A)) := characterExtensionAction χ
  constructor
  apply continuous_prod_of_discrete_right.mpr
  intro x
  exact (continuous_of_discreteTopology
    (f := fun a : Multiplicative A => (x.1 + x.2 a.toAdd, x.2))).comp χ.continuous
theorem

characterExtensionAction_inclusion

L76 ↗
EtaleFundamentalGroups.Cohomology.characterExtensionAction_inclusion
Documentation

The included coefficient group has trivial monodromy.

Source context 4 commands

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

noncomputable section
universe u v
namespace EtaleFundamentalGroups.Cohomology
variable {G : Type v} [Group G] [TopologicalSpace G]
  {A : Type u} [AddCommGroup A] [TopologicalSpace A]
  (χ : G →ₜ* Multiplicative A)
Lean source · full declaration
theorem characterExtensionAction_inclusion (g : G) (a : A) :
    let : DistribMulAction G (A × (A →+ A)) := characterExtensionAction χ
    g • (a, (0 : A →+ A)) = (a, 0) := by
  exact Prod.ext (add_zero a) rfl
theorem

characterExtensionAction_projection

L82 ↗
EtaleFundamentalGroups.Cohomology.characterExtensionAction_projection
Documentation

Projection to the endomorphism group has trivial monodromy.

Source context 4 commands

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

noncomputable section
universe u v
namespace EtaleFundamentalGroups.Cohomology
variable {G : Type v} [Group G] [TopologicalSpace G]
  {A : Type u} [AddCommGroup A] [TopologicalSpace A]
  (χ : G →ₜ* Multiplicative A)
Lean source · full declaration
theorem characterExtensionAction_projection (g : G) (x : A × (A →+ A)) :
    let : DistribMulAction G (A × (A →+ A)) := characterExtensionAction χ
    (g • x).2 = x.2 := rfl
theorem

characterExtensionAction_identityFiber

L87 ↗
EtaleFundamentalGroups.Cohomology.characterExtensionAction_identityFiber
Documentation

The fiber of the identity endomorphism recovers the original character.

Source context 4 commands

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

noncomputable section
universe u v
namespace EtaleFundamentalGroups.Cohomology
variable {G : Type v} [Group G] [TopologicalSpace G]
  {A : Type u} [AddCommGroup A] [TopologicalSpace A]
  (χ : G →ₜ* Multiplicative A)
Lean source · full declaration
theorem characterExtensionAction_identityFiber (g : G) :
    let : DistribMulAction G (A × (A →+ A)) := characterExtensionAction χ
    g • (0, AddMonoidHom.id A) = ((χ g).toAdd, AddMonoidHom.id A) := by
  exact Prod.ext (zero_add (χ g).toAdd) rfl

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