English
An element x in the mixed space is zero iff all of its norms at every place are zero.
Русский
Элемент x равен нулю тогда и только тогда, когда все нормы на местах равны нулю.
LaTeX
$$$\big(\forall w, \operatorname{normAtPlace}(w)(x) = 0\big) \iff x = 0.$$$
Lean4
/-- This is a technical result to ensure that the image of the `ℂ`-basis of `ℂ^n` defined in
`canonicalEmbedding.latticeBasis` is a `ℝ`-basis of the mixed space `ℝ^r₁ × ℂ^r₂`,
see `mixedEmbedding.latticeBasis`. -/
theorem disjoint_span_commMap_ker [NumberField K] :
Disjoint (Submodule.span ℝ (Set.range (canonicalEmbedding.latticeBasis K))) (LinearMap.ker (commMap K)) :=
by
refine LinearMap.disjoint_ker.mpr (fun x h_mem h_zero => ?_)
replace h_mem : x ∈ Submodule.span ℝ (Set.range (canonicalEmbedding K)) :=
by
refine (Submodule.span_mono ?_) h_mem
rintro _ ⟨i, rfl⟩
exact ⟨integralBasis K i, (canonicalEmbedding.latticeBasis_apply K i).symm⟩
ext1 φ
rw [Pi.zero_apply]
by_cases hφ : ComplexEmbedding.IsReal φ
· apply Complex.ext
· rw [← embedding_mk_eq_of_isReal hφ, ← commMap_apply_of_isReal K x ⟨φ, hφ, rfl⟩]
exact congrFun (congrArg (fun x => x.1) h_zero) ⟨InfinitePlace.mk φ, _⟩
·
rw [Complex.zero_im, ← Complex.conj_eq_iff_im, canonicalEmbedding.conj_apply _ h_mem,
ComplexEmbedding.isReal_iff.mp hφ]
· have := congrFun (congrArg (fun x => x.2) h_zero) ⟨InfinitePlace.mk φ, ⟨φ, hφ, rfl⟩⟩
cases embedding_mk_eq φ with
| inl h => rwa [← h, ← commMap_apply_of_isComplex K x ⟨φ, hφ, rfl⟩]
| inr h =>
apply RingHom.injective (starRingEnd ℂ)
rwa [canonicalEmbedding.conj_apply _ h_mem, ← h, map_zero, ← commMap_apply_of_isComplex K x ⟨φ, hφ, rfl⟩]
