isIntegral_of_profinite — Mathlib

English

G acts transitively on the prime ideals of B lying above a fixed prime of A; i.e., if P.under A = Q.under A then there exists g in G with Q = g • P.

Русский

G действует транзитивно на множестве простых идеалов B, лежащих над данным простым идеалом A; если P.under A = Q.under A, то существует g в G, такой что Q = g • P.

LaTeX

$$$\\exists g \\in G,\\ Q = g \\cdot P.$$$

Lean4

theorem isIntegral_of_profinite [Algebra.IsInvariant A B G] : Algebra.IsIntegral A B :=
  by
  constructor
  intro x
  obtain ⟨N, hN⟩ := ProfiniteGrp.exist_openNormalSubgroup_sub_open_nhds_of_one (stabilizer_isOpen G x) (one_mem _)
  have := (Algebra.IsInvariant.isIntegral A (FixedPoints.subalgebra A B N.1.1) (G ⧸ N.1.1)).1 ⟨x, fun g ↦ hN g.2⟩
  exact this.map (FixedPoints.subalgebra A B N.1.1).val

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