English
Equivalence between the quotient by orbit relations and the base infinite places.
Русский
Эквивалентность между полусоединением поRelation орбит и бесконечными местами базового поля.
LaTeX
$$$ \text{orbitRelEquiv} : \text{Quotient}(\mathrm{MulAction}.\mathrm{orbitRel}(\mathrm{AlgEquiv}(k,K), \mathrm{InfinitePlace}(K))) \simeq \mathrm{InfinitePlace}(k) $$$
Lean4
/-- The orbits of infinite places under the action of the Galois group are indexed by
the infinite places of the base field. -/
noncomputable def orbitRelEquiv [IsGalois k K] :
Quotient (MulAction.orbitRel (K ≃ₐ[k] K) (InfinitePlace K)) ≃ InfinitePlace k :=
by
refine Equiv.ofBijective (Quotient.lift (comap · (algebraMap k K)) fun _ _ e ↦ (mem_orbit_iff.mp e).symm) ⟨?_, ?_⟩
· rintro ⟨w⟩ ⟨w'⟩ e
exact Quotient.sound (mem_orbit_iff.mpr e.symm)
· intro w
obtain ⟨w', hw⟩ := comap_surjective (K := K) w
exact ⟨⟦w'⟧, hw⟩
