The finite-place completion comparison restricts to an inclusion of integer-unit groups: an integral unit on the adic-completion side has an integer-unit preimage on the absolute-value-completion side.
Source context 11 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField TensorProduct ValuativeRel NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
open ValuationTheory.Completion
variable
{K L : Type}
[Field K] [NumberField K]
[Field L] [NumberField L] [Algebra K L]
[FiniteDimensional K L] [IsGalois K L]
universe u
omit [NumberField L] [IsGalois K L] inLean source · full declaration
theorem exists_finitePlaceCompletionIntegerUnit_of_unitsEquiv_eq
(v₀ : HeightOneSpectrum (𝓞 K))
(x₀ :
(HeightOneSpectrum.adicAbv K v₀).Completionˣ)
(x : (v₀.adicCompletion K)ˣ)
(hx :
finitePlaceCompletionUnitsContinuousMulEquiv v₀ x₀ = x)
(hxUnit :
x ∈ (v₀.adicCompletionIntegers K).units) :
let vK := HeightOneSpectrum.adicAbv K v₀
let hvKna : IsNonarchimedean (vK : K → ℝ) :=
HeightOneSpectrum.isNonarchimedean_adicAbv K v₀
letI : Valued vK.Completion ℝ≥0 :=
finitePlaceCompletionValued vK hvKna
letI : ValuativeRel vK.Completion :=
finitePlaceCompletionValuativeRel vK hvKna
∃ x₀O : 𝒪[vK.Completion]ˣ,
integerUnitsToFieldUnits vK.Completion x₀O = x₀ := by
let vK := HeightOneSpectrum.adicAbv K v₀
let hvKna : IsNonarchimedean (vK : K → ℝ) :=
HeightOneSpectrum.isNonarchimedean_adicAbv K v₀
let : Valued vK.Completion ℝ≥0 :=
finitePlaceCompletionValued vK hvKna
let : ValuativeRel vK.Completion :=
finitePlaceCompletionValuativeRel vK hvKna
rw [Submonoid.mem_units_iff] at hxUnit
have hx₀norm :
‖(x₀ : vK.Completion)‖ ≤ 1 := by
have hval :=
congrArg
(fun q : (v₀.adicCompletion K)ˣ =>
(q : v₀.adicCompletion K)) hx
have hnorm :
‖finitePlaceCompletionRingHom v₀
(x₀ : vK.Completion)‖ =
‖(x₀ : vK.Completion)‖ :=
(finitePlaceCompletionRingHom_isometry v₀).norm_map_of_map_zero
(map_zero (finitePlaceCompletionRingHom v₀)) _
rw [← hnorm]
rw [show finitePlaceCompletionRingHom v₀
(x₀ : vK.Completion) = (x : v₀.adicCompletion K) by
exact hval]
exact norm_le_one_of_mem_adicCompletionIntegers v₀ hxUnit.1
have hx₀invnorm :
‖((x₀⁻¹ : vK.Completionˣ) : vK.Completion)‖ ≤ 1 := by
have hval :=
congrArg
(fun q : (v₀.adicCompletion K)ˣ =>
(q : v₀.adicCompletion K))
(congrArg Inv.inv hx)
have hnorm :
‖finitePlaceCompletionRingHom v₀
((x₀⁻¹ : vK.Completionˣ) : vK.Completion)‖ =
‖((x₀⁻¹ : vK.Completionˣ) : vK.Completion)‖ :=
(finitePlaceCompletionRingHom_isometry v₀).norm_map_of_map_zero
(map_zero (finitePlaceCompletionRingHom v₀)) _
rw [← hnorm]
rw [show finitePlaceCompletionRingHom v₀
((x₀⁻¹ : vK.Completionˣ) : vK.Completion) =
((x⁻¹ : (v₀.adicCompletion K)ˣ) :
v₀.adicCompletion K) by
exact hval]
exact norm_le_one_of_mem_adicCompletionIntegers v₀ hxUnit.2
let x₀O : 𝒪[vK.Completion]ˣ :=
{ val :=
⟨x₀,
(finitePlaceCompletion_mem_integers_iff_norm_le_one
vK hvKna (x₀ : vK.Completion)).2 hx₀norm⟩
inv :=
⟨x₀⁻¹,
by
simpa using
(finitePlaceCompletion_mem_integers_iff_norm_le_one
vK hvKna
((x₀⁻¹ : vK.Completionˣ) :
vK.Completion)).2 hx₀invnorm⟩
val_inv := by
apply Subtype.ext
simp
inv_val := by
apply Subtype.ext
simp }
refine ⟨x₀O, ?_⟩
apply Units.ext
rfl