IdeleGroup.finiteComponent_norm_eq_prod_extensions
The relative-tensor coordinate form underlying the public finite-place formula below.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped BigOperators NumberField TensorProduct NumberField.LiesOver
open NumberField IsDedekindDomain
noncomputable section
namespace IdeleGroup
open AlgebraicNumberTheory.Valuations
universe u v
variable
(K : Type u) (L : Type v)
[Field K] [NumberField K]
[Field L] [NumberField L] [Algebra K L]Lean source · full declaration
theorem finiteComponent_norm_eq_prod_extensions
(v : HeightOneSpectrum (𝓞 K))
(a : IdeleGroup L) :
let vK := HeightOneSpectrum.adicAbv K v
let hvK : vK.IsNontrivial :=
RayClass.adicAbv_isNontrivial v
let z :=
(relativeIdeleBaseChangeMulEquiv
(K := K) (L := L)).symm a
let x :=
RelativeIdeleGroup.finiteComponent
(K := K) (L := L) v z
letI :=
completionTensorDecomposition_extensionFintype
(K := K) (L := L) vK hvK
letI : ∀ w : AbsoluteValueExtension vK L,
Algebra vK.Completion w.1.Completion :=
fun w =>
AbsoluteValue.completionAlgebra vK w.1 w.2
letI : ∀ w : AbsoluteValueExtension vK L,
Module.Finite vK.Completion w.1.Completion :=
fun w =>
completionModuleFinite vK hvK w
Units.mapEquiv
(_root_.relativeFinitePlaceCompletionAlgEquiv
(K := K) v).symm.toMulEquiv
(finiteComponent v (norm K L a)) =
∏ w : AbsoluteValueExtension vK L,
Units.map (Algebra.norm vK.Completion)
(_root_.finitePlaceLocalTensorDecompositionUnitsComponent
(K := K) (L := L) v w x) := by
classical
let vK := HeightOneSpectrum.adicAbv K v
let hvK : vK.IsNontrivial :=
RayClass.adicAbv_isNontrivial v
let e :=
relativeIdeleBaseChangeMulEquiv
(K := K) (L := L)
let z := e.symm a
let x :=
RelativeIdeleGroup.finiteComponent
(K := K) (L := L) v z
let :=
completionTensorDecomposition_extensionFintype
(K := K) (L := L) vK hvK
let : ∀ w : AbsoluteValueExtension vK L,
Algebra vK.Completion w.1.Completion :=
fun w =>
AbsoluteValue.completionAlgebra vK w.1 w.2
let : ∀ w : AbsoluteValueExtension vK L,
Module.Finite vK.Completion w.1.Completion :=
fun w =>
completionModuleFinite vK hvK w
have hz : e z = a :=
e.apply_symm_apply a
change
Units.mapEquiv
(_root_.relativeFinitePlaceCompletionAlgEquiv
(K := K) v).symm.toMulEquiv
(finiteComponent v (norm K L a)) =
∏ w : AbsoluteValueExtension vK L,
Units.map (Algebra.norm vK.Completion)
(_root_.finitePlaceLocalTensorDecompositionUnitsComponent
(K := K) (L := L) v w x)
rw [← hz, norm_relativeIdeleBaseChangeMulEquiv,
RelativeIdeleGroup.finiteComponent_norm]
apply Units.ext
change
(_root_.relativeFinitePlaceCompletionAlgEquiv
(K := K) v).symm
(Algebra.norm (v.adicCompletion K)
(x : v.adicCompletion K ⊗[K] L)) =
(((∏ w : AbsoluteValueExtension vK L,
Units.map (Algebra.norm vK.Completion)
(_root_.finitePlaceLocalTensorDecompositionUnitsComponent
(K := K) (L := L) v w x)) :
vK.Completionˣ) : vK.Completion)
let x' : (vK.Completion ⊗[K] L)ˣ :=
Units.mapEquiv
(_root_.relativeFinitePlaceLocalTensorAlgEquiv
(K := K) (L := L) v).symm.toMulEquiv x
calc
(_root_.relativeFinitePlaceCompletionAlgEquiv
(K := K) v).symm
(Algebra.norm (v.adicCompletion K)
(x : v.adicCompletion K ⊗[K] L)) =
Algebra.norm vK.Completion
(x' : vK.Completion ⊗[K] L) := by
exact
map_norm_tensorProduct_baseChange
(K := K) (L := L)
(_root_.relativeFinitePlaceCompletionAlgEquiv
(K := K) v).symm.toAlgHom
(x : v.adicCompletion K ⊗[K] L)
_ = ∏ w : AbsoluteValueExtension vK L,
Algebra.norm vK.Completion
(completionTensorDecomposition_left
(K := K) (L := L) vK hvK
(x' : vK.Completion ⊗[K] L) w) := by
exact
RelativeIdeleGroup.localNorm_units_eq_prod
vK hvK x'
_ =
(((∏ w : AbsoluteValueExtension vK L,
Units.map (Algebra.norm vK.Completion)
(_root_.finitePlaceLocalTensorDecompositionUnitsComponent
(K := K) (L := L) v w x)) :
vK.Completionˣ) : vK.Completion) := by
change _ = Units.coeHom vK.Completion _
rw [map_prod]
apply Finset.prod_congr rfl
intro w _
rfl