Theorems · Theorem · commutative algebra

Algebra.IsInvariant.exists_smul_of_under_eq

∀ (A : Type u_1) (B : Type u_2) (G : Type u_3) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [inst_3 : Group G] [inst_4 : MulSemiringAction G B] [Algebra.IsInvariant A B G] [Finite G] [SMulCommClass G A B]
  (P Q : Ideal B) [hP : P.IsPrime] [hQ : Q.IsPrime], Ideal.under A P = Ideal.under A Q → ∃ g, Q = g • P

G acts transitively on the prime ideals of B above a given prime ideal of A.

Defined in

Mathlib.RingTheory.Invariant.Basic

Cited by

5 results in Mathlib

Foundations

Depth 98 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingAlgebraGroupMulSemiringActionAlgebra.IsInvariantFiniteSMulCommClassIdeal.IsPrimeIdeal.IsPrime