Module

LaurentCoverAutomorphisms.lean

Nyll.AnabelianGeometry.GeometricFundamentalGroup.LaurentCoverAutomorphisms

1 declaration indexed from sourceView source ↗

Module documentation

Cyclic automorphisms of connected finite etale covers of the multiplicative line

The original cover is affine. Its actual section algebra is finite etale over the Laurent polynomial ring and has connected spectrum. Pullback of sections by inverse cover automorphisms gives an injective group homomorphism into its cyclic algebra automorphism group.

Imports4

Nyll.AnabelianGeometry.GeometricFundamentalGroup.LaurentEtaleAutomorphisms
Nyll.SchemeTheory.Pi1.FiniteEtale.Basic
Mathlib.AlgebraicGeometry.AffineScheme
Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Imported by2

theorem

isCyclic_aut_of_connected_finite_etale_laurent

L28 ↗

AnabelianGeometry.GeometricFundamentalGroup.isCyclic_aut_of_connected_finite_etale_laurent

Documentation

The categorical automorphism group of an actual connected finite etale cover of the multiplicative line is cyclic in characteristic zero.

Source context 3 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
namespace AnabelianGeometry.GeometricFundamentalGroup

Lean source · statement

theorem isCyclic_aut_of_connected_finite_etale_laurent
    {K : Type} [Field K] [IsAlgClosed K] [CharZero K]
    (Y : FiniteEtale (Spec (CommRingCat.of (LaurentPolynomial K))))
    [ConnectedSpace Y.left] : IsCyclic (Aut Y)

Module documentation

Cyclic automorphisms of connected finite etale covers of the multiplicative line

Declarations

isCyclic_aut_of_connected_finite_etale_laurent