ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn

English

If p is prime over A and P, Q lie over p, there exists σ ∈ Aut_A(B) such that map σ P = Q.

Русский

Если p – простой над A, P и Q лежат над p, существует σ ∈ Aut_A(B) такого, что map σ P = Q.

LaTeX

$$$\\exists \\sigma : B \\simeq_{A} B,\\; \\mathrm{map}\\; \\sigma\\; P = Q$$$

Lean4

/-- The form of the **fundamental identity** in the case of Galois extension. -/
theorem ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn [IsGalois K L] :
    (primesOver p B).ncard * (ramificationIdxIn p B * inertiaDegIn p B) = Module.finrank K L :=
  by
  have : FaithfulSMul A B := FaithfulSMul.of_field_isFractionRing A B K L
  rw [← smul_eq_mul, ← coe_primesOverFinset hpb B, Set.ncard_coe_finset, ← Finset.sum_const]
  rw [← sum_ramification_inertia B K L hpb]
  apply Finset.sum_congr rfl
  intro P hp
  rw [← Finset.mem_coe, coe_primesOverFinset hpb B] at hp
  obtain ⟨_, _⟩ := hp
  rw [ramificationIdxIn_eq_ramificationIdx p P K L, inertiaDegIn_eq_inertiaDeg p P K L]

Похожие утверждения