The cover is the spectrum of the actual monic quotient R[T]/(T^n-u). Its étaleness is reused from the algebraic-curve library. Lying over proves surjectivity, and the adjoined root is explicitly a unit. These are the geometric local inputs to the Kummer sequence; no cohomology comparison or local lifting assumption is used.
The actual algebra used to extract an nth root of a unit.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Polynomial
namespace EtaleCohomologyabbrev kummerRootAlgebra {R : Type u} [CommRing R] (n : ℕ) (a : Rˣ)The defining relation in the actual root algebra.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Polynomial
namespace EtaleCohomologytheorem kummerRootAlgebra_root_pow {R : Type u} [CommRing R] (n : ℕ) (a : Rˣ) :
AdjoinRoot.root (X ^ n - C (a : R)) ^ n =
algebraMap R (kummerRootAlgebra n a) (a : R)The adjoined root is an actual unit, with inverse t^(n-1) u^(-1).
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Polynomial
namespace EtaleCohomologydef kummerRootUnit {R : Type u} [CommRing R] {n : ℕ} (hn : 0 < n) (a : Rˣ) :
(kummerRootAlgebra n a)ˣSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Polynomial
namespace EtaleCohomologytheorem kummerRootUnit_pow {R : Type u} [CommRing R] {n : ℕ}
(hn : 0 < n) (a : Rˣ) :
kummerRootUnit hn a ^ n =
Units.map (algebraMap R (kummerRootAlgebra n a)).toMonoidHom aThe actual root cover is finite étale when n is invertible.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Polynomial
namespace EtaleCohomologytheorem kummerRootCover_isFiniteEtale {R : Type u} [CommRing R]
(n : ℕ) (a : Rˣ) (hn : IsUnit (n : R)) :
IsFiniteEtale (Spec.map (CommRingCat.ofHom
(algebraMap R (kummerRootAlgebra n a))))Lying over proves that every point of the affine base is covered. No irreducibility of the Kummer polynomial is required.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Polynomial
namespace EtaleCohomologytheorem kummerRootCover_surjective {R : Type u} [CommRing R]
{n : ℕ} (hn : 0 < n) (a : Rˣ) :
Function.Surjective (Spec.map (CommRingCat.ofHom
(algebraMap R (kummerRootAlgebra n a))))The actual root cover has constant degree n, including when it is disconnected. This follows from the monic power basis, not from an assumed degree comparison.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Polynomial
namespace EtaleCohomologytheorem kummerRootCover_finrank {R : Type u} [CommRing R]
{n : ℕ} (hn : 0 < n) (a : Rˣ) (x : Spec (.of R)) :
(Spec.map (CommRingCat.ofHom
(algebraMap R (kummerRootAlgebra n a)))).finrank x = n