English
In a Galois setting, the complement cardinalities of unramified places relate to orbit data and finiteness degree.
Русский
В галлоzовом окружении кардинальности дополнения безразветвленных мест связаны с данными орбит и степенью расширения.
LaTeX
$$For [IsGalois k K], #({w : InfinitePlace K | w.IsUnramified k})ᶜ = #({w : InfinitePlace k | w.IsUnramifiedIn K} : Finset)ᶜ * (finrank k K / 2).$$
Lean4
theorem card_isUnramified_compl [NumberField k] [IsGalois k K] :
#({w : InfinitePlace K | w.IsUnramified k} : Finset _)ᶜ =
#({w : InfinitePlace k | w.IsUnramifiedIn K} : Finset _)ᶜ * (finrank k K / 2) :=
by
letI := Module.Finite.of_restrictScalars_finite ℚ k K
rw [← IsGalois.card_aut_eq_finrank,
Finset.card_eq_sum_card_fiberwise (f := (comap · (algebraMap k K))) (t :=
({w : InfinitePlace k | w.IsUnramifiedIn K} : Finset _)ᶜ),
← smul_eq_mul, ← sum_const]
· refine sum_congr rfl (fun w hw ↦ ?_)
obtain ⟨w, rfl⟩ := comap_surjective (K := K) w
rw [compl_filter, mem_filter_univ] at hw
trans Finset.card (MulAction.orbit (K ≃ₐ[k] K) w).toFinset
· congr; ext w'
rw [mem_filter, compl_filter, mem_filter_univ, @eq_comm _ (comap w' _), Set.mem_toFinset, mem_orbit_iff,
and_iff_right_iff_imp]
intro e; rwa [← isUnramifiedIn_comap, ← e]
· rw [Nat.card_eq_fintype_card, ← MulAction.card_orbit_mul_card_stabilizer_eq_card_group _ w, ←
Nat.card_eq_fintype_card (α := Stab w), InfinitePlace.card_stabilizer, if_neg, Nat.mul_div_cancel _ zero_lt_two,
Set.toFinset_card]
rwa [← isUnramifiedIn_comap]
· simp [Set.MapsTo, isUnramifiedIn_comap]
