NYLL
Module

LaurentEtaleAutomorphisms.lean

Nyll.AnabelianGeometry.GeometricFundamentalGroup.LaurentEtaleAutomorphisms
1 declaration indexed from sourceView source ↗

Module documentation

Automorphisms of actual connected finite etale Laurent algebras

Connectedness of the spectrum supplies domain and normality from the finite-etale hypotheses. Thus the original algebra is its base ring's integral closure in its actual fraction field. Restriction of automorphisms identifies its automorphism group with the proved cyclic generic Galois group. Normality and a generic-field comparison are not additional assumptions.

Imports5
Imported by2

Declarations

theorem

isCyclic_algEquiv_of_connected_finite_etale_laurent

L30 ↗
AnabelianGeometry.GeometricFundamentalGroup.isCyclic_algEquiv_of_connected_finite_etale_laurent
Documentation

Every connected finite etale Laurent algebra over an algebraically closed field of characteristic zero has cyclic automorphism group. Domain and normality are consequences.

Source context 3 commands

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

noncomputable section
open EtaleFundamentalGroups
namespace AnabelianGeometry.GeometricFundamentalGroup
Lean source · statement
theorem isCyclic_algEquiv_of_connected_finite_etale_laurent
    {K T : Type} [Field K] [IsAlgClosed K] [CharZero K]
    [CommRing T] [Algebra (LaurentPolynomial K) T]
    [Module.Finite (LaurentPolynomial K) T] [Algebra.Etale (LaurentPolynomial K) T]
    [ConnectedSpace (PrimeSpectrum T)] : IsCyclic (T ≃ₐ[LaurentPolynomial K] T)

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