finite_of_isInvariant — Mathlib

English

If the action is invariant and B/Q is separable over A/P, then B/Q is finite as a module over A/P.

Русский

Если действие инвариантно и B/Q разделимо над A/P, то B/Q является конечным модулем над A/P.

LaTeX

$$$\\text{Module.Finite} (A / P) (B / Q).$$$

Lean4

/-- If the extension `B/Q` over `A/P` is separable, then it is finite dimensional. -/
theorem finite_of_isInvariant [P.IsMaximal] [Q.IsMaximal] [SMulCommClass G A B] [Algebra.IsSeparable (A ⧸ P) (B ⧸ Q)] :
    Module.Finite (A ⧸ P) (B ⧸ Q) :=
  by
  have : IsGalois (A ⧸ P) (B ⧸ Q) := { __ := Ideal.Quotient.normal (A := A) G P Q }
  have := Finite.of_surjective _ (Ideal.Quotient.stabilizerHom_surjective G P Q)
  exact IsGalois.finiteDimensional_of_finite _ _

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