ModuleCompositum.lean
Nyll.EtaleFundamentalGroups.Kummer.UnitAbsorption.Compositum
4 declarations indexed from sourceView source ↗ Module documentation
The actual compositum in finite-etale unit absorption
The unit-root construction used in the characteristic-zero DVR case chooses delta over the target field and then puts alpha = delta * pi. This file records two facts which are needed to use that construction as an Abhyankar base change.
- The chosen field factor
L(delta) is exactly the actual compositum of the
embedded target field and the pure radical field K(alpha).
- A chosen root of
X ^ n - unit has a monic integral minimal polynomial
whose adjoined-root algebra is finite etale. Thus the particular generic field factor selected by delta, rather than merely the whole split Kummer algebra, has a finite-etale integral model.
Declarations
EtaleFundamentalGroups.Kummer.restrictScalars_adjoin_eq_fieldRange_sup_adjoin_of_eq_mul
DocumentationIf alpha = delta * pi with pi nonzero in the embedded target field, then adjoining delta over the target is the actual compositum of the target and the pure radical field generated by alpha over the base.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups.Kummer
open Polynomial
universe u v w x
EtaleFundamentalGroups.Kummer.exists_finiteEtale_integralFactor_of_pow_eq_unit
DocumentationA chosen generic field factor of a Kummer unit-root algebra descends to a finite-etale monogenic algebra over an integrally closed fraction-ring base.
The polynomial q is produced as the integral minimal polynomial of the chosen root. Its generic fibre is the field factor L(delta), while its integral adjoined-root algebra is finite etale.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups.Kummer
open Polynomial
universe u v w x
EtaleFundamentalGroups.Kummer.exists_finiteEtale_unitFactor_for_prescribed_uniformizerRoot
DocumentationUnit absorption for a prescribed pure uniformizer root.
This is the form used when a larger root cover has exponent N divisible by the original ramification index e: if beta ^ N = varpi, take alpha = beta ^ (N / e). The theorem does not require the pure radical extension generated by alpha to be normal.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups.Kummer
open Polynomial
universe u v w x
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
EtaleFundamentalGroups.Kummer.exists_finiteEtale_unitAbsorption_actualCompositum
DocumentationIn residue characteristic zero, the uniformizer radical supplied by unit absorption has an actual compositum with the target whose chosen integral model is finite etale over the target valuation ring.
Unlike the full Kummer unit-root algebra, AdjoinRoot q is the particular integral factor selected by delta; its generic fibre is identified with L(delta), and L(delta) is identified with the actual compositum L * K(alpha) inside AlgebraicClosure L.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups.Kummer
open Polynomial
universe u v w x
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
Lean source · full declarationtheorem exists_finiteEtale_unitAbsorption_actualCompositum
{K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
(base : DVF.{u, w} K) (target : DVF.{v, x} L)
[base.valuation.HasExtension target.valuation]
[CharZero base.residueField] :
let n := ramificationIndex base target
∃ (varpi : base.valuationSubring) (pi : target.valuationSubring)
(unit : target.valuationSubringˣ)
(delta alpha : AlgebraicClosure L) (q : target.valuationSubring[X])
(unitFactorEquiv :
AdjoinRoot (q.map (algebraMap target.valuationSubring L)) ≃ₐ[L]
IntermediateField.adjoin L ({delta} : Set (AlgebraicClosure L)))
(radicalEquiv :
AdjoinRoot (X ^ n - C (varpi : K)) ≃ₐ[K]
IntermediateField.adjoin K ({alpha} : Set (AlgebraicClosure L))),
base.valuation.IsUniformizer (varpi : K) ∧
target.valuation.IsUniformizer (pi : L) ∧
integerMap base target varpi =
(unit : target.valuationSubring) * pi ^ n ∧
delta ^ n = algebraMap L (AlgebraicClosure L) (unit : L) ∧
alpha = delta * algebraMap L (AlgebraicClosure L) (pi : L) ∧
alpha ^ n =
algebraMap K (AlgebraicClosure L) (varpi : K) ∧
q.Monic ∧
q.map (algebraMap target.valuationSubring L) =
minpoly L delta ∧
q ∣ X ^ n - C (unit : target.valuationSubring) ∧
Algebra.Etale target.valuationSubring (AdjoinRoot q) ∧
Module.Finite target.valuationSubring (AdjoinRoot q) ∧
(IntermediateField.adjoin L
({delta} : Set (AlgebraicClosure L))).restrictScalars K =
(IsScalarTower.toAlgHom K L
(AlgebraicClosure L)).fieldRange ⊔
IntermediateField.adjoin K
({alpha} : Set (AlgebraicClosure L)) ∧
unitFactorEquiv
(AdjoinRoot.root
(q.map
(algebraMap target.valuationSubring L))) =
IntermediateField.AdjoinSimple.gen L delta ∧
radicalEquiv
(AdjoinRoot.root
(X ^ n - C (varpi : K))) =
IntermediateField.AdjoinSimple.gen K alpha := by
let n := ramificationIndex base target
have hn_ne : n ≠ 0 := by
simpa [n, ramificationIndex] using
(Ideal.IsDedekindDomain.ramificationIdx'_ne_zero
(maximalIdeal_map_integerMap_ne_bot base target)
(IsLocalRing.maximalIdeal.isMaximal target.valuationSubring).isPrime
(maximalIdeal_map_integerMap_le base target))
have hn : 0 < n := Nat.pos_of_ne_zero hn_ne
have hnBase : IsUnit (n : base.valuationSubring) := by
apply (base.residue_ne_zero_iff_isUnit (n : base.valuationSubring)).mp
simpa using (Nat.cast_ne_zero.mpr hn_ne : (n : base.residueField) ≠ 0)
have hnTarget : IsUnit (n : target.valuationSubring) := by
simpa using hnBase.map (integerMap base target)
obtain ⟨varpi, pi, unit, delta, alpha, factorEquiv, radicalEquiv,
hvarpi, hpi, hvarpiPrime, hdecomp, hWholeEtale, hWholeFinite,
hdelta, hMinpolyDvd, hdeltaSeparable, halpha, halphaPow,
hFactorRoot, hRadicalRoot⟩ :=
exists_finiteEtale_unitAbsorption_uniformizerRadical base target
let : IsFractionRing target.valuationSubring L :=
target.valuationSubring_isFractionRing
let : IsIntegrallyClosed target.valuationSubring :=
target.valuationSubring_isIntegrallyClosed
obtain ⟨q, unitFactorEquiv, hqMonic, hqMap, hqDvd,
hqEtale, hqFinite, hUnitFactorRoot⟩ :=
exists_finiteEtale_integralFactor_of_pow_eq_unit
(B := target.valuationSubring) (L := L)
(Omega := AlgebraicClosure L) hn hnTarget unit delta (by
simpa using hdelta)
have hCompositum :=
restrictScalars_adjoin_eq_fieldRange_sup_adjoin_of_eq_mul
(K := K) (L := L) (Omega := AlgebraicClosure L)
delta alpha (pi : L) halpha hpi.ne_zero
exact ⟨varpi, pi, unit, delta, alpha, q, unitFactorEquiv, radicalEquiv,
hvarpi, hpi, hdecomp, hdelta, halpha, halphaPow, hqMonic, hqMap,
hqDvd, hqEtale, hqFinite, hCompositum, hUnitFactorRoot,
hRadicalRoot⟩