English
The norm of a unit in the ring of integers is 1.
Русский
Норма единицы в кольце целых чисел равна 1.
LaTeX
$$$ \| \text{mixedEmbedding}(K, u) \| = 1 $$$
Lean4
/-- The `Equiv` between `index K` and `K →+* ℂ` defined by sending a real infinite place `w` to
the unique corresponding embedding `w.embedding`, and the pair `⟨w, 0⟩` (resp. `⟨w, 1⟩`) for a
complex infinite place `w` to `w.embedding` (resp. `conjugate w.embedding`). -/
def indexEquiv : (index K) ≃ (K →+* ℂ) :=
by
refine Equiv.ofBijective (fun c => ?_) ((Fintype.bijective_iff_surjective_and_card _).mpr ⟨?_, ?_⟩)
·
cases c with
| inl w => exact w.val.embedding
| inr wj =>
rcases wj with ⟨w, j⟩
exact if j = 0 then w.val.embedding else ComplexEmbedding.conjugate w.val.embedding
· intro φ
by_cases hφ : ComplexEmbedding.IsReal φ
· exact ⟨Sum.inl (InfinitePlace.mkReal ⟨φ, hφ⟩), by simp [embedding_mk_eq_of_isReal hφ]⟩
· by_cases hw : (InfinitePlace.mk φ).embedding = φ
· exact ⟨Sum.inr ⟨InfinitePlace.mkComplex ⟨φ, hφ⟩, 0⟩, by simp [hw]⟩
· exact ⟨Sum.inr ⟨InfinitePlace.mkComplex ⟨φ, hφ⟩, 1⟩, by simp [(embedding_mk_eq φ).resolve_left hw]⟩
· rw [Embeddings.card, ← mixedEmbedding.finrank K, ← Module.finrank_eq_card_basis (stdBasis K)]
