Decomposition subgroup for a place (AbsoluteValue) #
(To be written)
References:
- [J. W. S. Cassels, A. Frohlich, editors, Algebraic Number Theory][cassels1967algebraic]
- [J. Neukirch, Algebraic Number Theory][Neukirch1992]
Lemmas should go mathlib #
If a < b, b, c are positive and c ≠ 1, then there are m : ℕ and n : ℤ
such that the power c ^ n is strictly between a ^ m and b ^ m.
TODO: go mathlib and add exists_pow_btwn_pow_of_lt
If a < b, b, c are positive and c ≠ 1, then there are m : ℕ and n : ℤ
such that 1 is strictly between a ^ m * c ^ n and b ^ m * c ^ n.
TODO: go mathlib
TODO: go mathlib
If a < b, b, c, d are positive and c ≠ 1, e is any element, then there are
m : ℕ and n : ℤ such that a ^ m * c ^ n < d and e < b ^ m * c ^ n.
TODO: go mathlib
Action on absolute values #
Ring isomorphisms act on the left on the absolute values by σ • v := v ∘ σ⁻¹.
Equations
- AbsoluteValue.instMulActionRingEquiv K S = { smul := fun (σ : K ≃+* K) (v : AbsoluteValue K S) => v.comp ⋯, mul_smul := ⋯, one_smul := ⋯ }
Algebra isomorphisms act on the left on the absolute values by σ • v := v ∘ σ⁻¹.
Equations
- AbsoluteValue.instMulActionAlgEquiv F K S = { smul := fun (σ : K ≃ₐ[F] K) (v : AbsoluteValue K S) => v.comp ⋯, mul_smul := ⋯, one_smul := ⋯ }
Decomposition subgroup for a place #
The decomposition subgroup Dᵥ(K/F) in Gal(K/F) for a place v of K consists of all σ
such that v ∘ σ = v. See [cassels1967algebraic], Chapter VII, §1.
This definition also works for infinite places.
Note: Here we use def but not abbrev because sometimes simp lemmas for MulAction.stabilizer
are not desired (will introduce σ⁻¹).
Equations
- AbsoluteValue.decompositionSubgroup F v = MulAction.stabilizer (K ≃ₐ[F] K) v
Instances For
The elements in decomposition subgroup preserve the set {x | v x ≤ y} for all y.
If K / F is algebraic, then the decomposition subgroup Dᵥ(K/F) is also the subgroup
consists of all σ preserving the set {x | v x ≤ 1}.
NOTE: This is not true if K / F is not algebraic, for example, when K is the fraction field of
the valuation ring $\bigcup_{n=1}^\infty F⟦X^{1/n}⟧$, k ≥ 2 is a fixed positive integer, σ is
$X^{1/n} \mapsto X^{k/n}$, then it preserves the valuation ring but doesn't preserve the valuation.
The elements in decomposition subgroup are continuous in v-adic topology.
If K / F is algebraic, then an element is contained in the decomposition subgroup of v
if and only if it is continuous under the v-adic topology.
Our definition is the same as ValuationSubring.decompositionSubgroup for finite places.
If L / K / F is an extension tower with L / F Galois, v is a place of L, then
Dᵥ(L/K) = Dᵥ(L/F) ⊓ Gal(L/K).
If L / K / F is an extension tower with L / F Galois, v is a place of L, then
Dᵥ(L/K) ≤ Dᵥ(L/F).
Decomposition subgroup for an infinite place is either trivial or ℤ/2ℤ. This is because the
decomposition subgroup can be viewed as Galois group of completions of fields with respect to
valuations (didn't formalized yet), in the archimedean case they must be ℝ or ℂ.
If v : ι → AbsoluteValue R S is a finite collection of non-trivial and pairwise inequivalent
absolute values, then for any ε > 0 and any i : ι there is some z : R such that
v i (z - 1) < ε and v j z < ε for all j ≠ i.
TODO: go mathlib
A version of Approximation Theorem: if v : ι → AbsoluteValue R S is a finite collection
of non-trivial and pairwise inequivalent absolute values, a : ι → R is a sequence of elements
in R, then for any ε > 0 there is some x : R such that v i (x - a i) < ε for all i.
See [Neukirch1992], II.3.4.
TODO: go mathlib
If K / F is an algebraic extension, then any place v of F can be extended to K.
(Is this correct?)
If K / F is a normal extension, then any two places of K which coincide when
restrict to F are conjugate by an element of Gal(K/F).
See [Neukirch1992], II.9.1.
If L / K / F is an extension tower, L / F and K / F are Galois, v and w are places of
K and L, respectively, such that w lies over v, then the image of D_w(L/F) in Gal(K/F)
is equal to Dᵥ(K/F).