English
Equivalence between unramified_in over K and unramified over k via comap (symmetric version).
Русский
Эквивалентность между безразветвленностью в K и над k через comap (симметричная версия).
LaTeX
$$(w.IsUnramifiedIn_K) ↔ (w.IsUnramified_k) under comap equivalence.$$
Lean4
theorem card_isUnramified [NumberField k] [IsGalois k K] :
#{w : InfinitePlace K | w.IsUnramified k} = #{w : InfinitePlace k | w.IsUnramifiedIn K} * finrank k K :=
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}),
← smul_eq_mul, ← sum_const]
· refine sum_congr rfl (fun w hw ↦ ?_)
obtain ⟨w, rfl⟩ := comap_surjective (K := K) w
rw [mem_filter_univ] at hw
trans #(MulAction.orbit (K ≃ₐ[k] K) w).toFinset
· congr; ext w'
rw [mem_filter, mem_filter_univ, Set.mem_toFinset, mem_orbit_iff, @eq_comm _ (comap w' _), 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), card_stabilizer, if_pos, mul_one, Set.toFinset_card]
rwa [← isUnramifiedIn_comap]
· simp [Set.MapsTo, isUnramifiedIn_comap]
