NYLL
Module

FinitePlaceDecompositionSplit.lean

Nyll.SawinTotallyRealTowers.FinitePlaceDecompositionSplit
1 declaration indexed from sourceView source ↗

Module documentation

Absolute decomposition at a completely split finite place

Restrict the chosen absolute valuation to the actual finite Galois layer. An absolute decomposition automorphism preserves this restricted valuation class. Complete splitting makes its decomposition group trivial, independently of the chosen exact extension of the base absolute value.

Imports6
Imported by2

Declarations

theorem

finitePlaceAbsoluteDecomposition_restrictNormal_eq_one_of_splitsCompletely

L32 ↗
ClassFieldTower.Sawin.finitePlaceAbsoluteDecomposition_restrictNormal_eq_one_of_splitsCompletely
Documentation

At a completely split place, every element of the actual absolute decomposition subgroup restricts trivially to the finite Galois layer.

Source context 4 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
namespace ClassFieldTower.Sawin
open ClassFieldTower.Martinet.Shafarevich AlgebraicNumberTheory.Valuations
Lean source · statement
theorem finitePlaceAbsoluteDecomposition_restrictNormal_eq_one_of_splitsCompletely
    (F : Type) [Field F] [NumberField F]
    (M : FiniteGaloisIntermediateField F (AlgebraicClosure F))
    (v : HeightOneSpectrum (𝓞 F))
    (hsplit : FinitePlaceSplitsCompletely (K := F) (L := M) v)
    (σ : finitePlaceAbsoluteDecompositionGroup F v) :
    AlgEquiv.restrictNormalHom M σ.1 = 1

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