Theorems · Theorem · field theory

Polynomial.Splits.toPermHom_apply_eq_one_or_isSwap_of_ncard_le_of_mem_inertia

∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [inst_3 : IsDomain S]
  {G : Type u_3} [inst_4 : Group G] [inst_5 : MulSemiringAction G S] [inst_6 : SMulCommClass G R S] {f : Polynomial R}
  [inst_7 : DecidableEq ↑(f.rootSet S)],
  (Polynomial.map (algebraMap R S) f).Splits →
    ∀ (p : Ideal S) [inst_8 : p.IsPrime],
      (f.rootSet S).ncard ≤ (f.rootSet (S ⧸ p)).ncard + 1 →
        ∀ g ∈ Ideal.inertia G p,
          (MulAction.toPermHom G ↑(f.rootSet S)) g = 1 ∨ ((MulAction.toPermHom G ↑(f.rootSet S)) g).IsSwap

If the roots of f in S have at most one collision mod p, then a MulSemiringAction on the roots in S must be the identity permutation or a transposition. Such polynomials are called Morse functions in Section 4.4 of [serre-galois].

Defined in

Mathlib.RingTheory.Polynomial.Morse

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraIsDomainGroupMulSemiringActionSMulCommClassDecidableEqIdeal.IsPrime