English
Under IsGalois K L, the action of AlgEquiv K L L on primesOver p B is pretransitive: for any two P,Q over p there exists σ with map σ P = Q.
Русский
При IsGalois K L действие AlgEquiv K L L на primesOver p B предтранситивно: для любых P,Q над p существует σ s.t. map σ P = Q.
LaTeX
$$$\\text{MulAction.IsPretransitive} (\\mathrm{AlgEquiv}\\ K L L) (p.primesOver B).Elem$$$
Lean4
/-- Let `R` be a domain of characteristic 0, finite rank over `ℤ`, `S` be a Dedekind domain
that is a finite `R`-algebra. Let `p` be a prime of `S`, then `p` is unramified iff `e(p) = 1`. -/
theorem isUnramifiedAt_iff_of_isDedekindDomain {p : Ideal S} [p.IsPrime] [IsDedekindDomain S] [EssFiniteType R S]
[IsDomain R] [Module.Finite ℤ R] [CharZero R] [Algebra.IsIntegral R S] (hp : p ≠ ⊥) :
Algebra.IsUnramifiedAt R p ↔ e(p|R) = 1 :=
by
rw [isUnramifiedAt_iff_map_eq R (p.under R) p, and_iff_right,
Ideal.IsDedekindDomain.ramificationIdx_eq_one_iff hp Ideal.map_comap_le]
have : Finite (R ⧸ p.under R) := Ideal.finiteQuotientOfFreeOfNeBot _ (mt Ideal.eq_bot_of_comap_eq_bot hp)
have : Finite ((p.under R).ResidueField) := IsLocalization.finite _ (nonZeroDivisors (R ⧸ p.under R))
infer_instance
