Unramified algebras over fields

Main results

Let K be a field, A be a K-algebra and L be a field extension of K.

• Algebra.FormallyUnramified.bijective_of_isAlgClosed_of_isLocalRing: If A is K-unramified and K is alg-closed, then K = A.
• Algebra.FormallyUnramified.isReduced_of_field: If A is K-unramified then A is reduced.
• Algebra.FormallyUnramified.iff_isSeparable: L is unramified over K iff L is separable over K.

References

• B. Iversen, Generic Local Structure of the Morphisms in Commutative Algebra

theorem Algebra.FormallyUnramified.of_isSeparable (K : Type u_1) (L : Type u_3) [Field K] [Field L] [Algebra K L] [Algebra.IsSeparable K L] : FormallyUnramified K L

theorem Algebra.FormallyUnramified.bijective_of_isAlgClosed_of_isLocalRing (K : Type u_1) (A : Type u_2) [Field K] [CommRing A] [Algebra K A] [FormallyUnramified K A] [EssFiniteType K A] [IsAlgClosed K] [IsLocalRing A] : Function.Bijective ⇑(algebraMap K A)

theorem Algebra.FormallyUnramified.isField_of_isAlgClosed_of_isLocalRing (K : Type u_1) (A : Type u_2) [Field K] [CommRing A] [Algebra K A] [FormallyUnramified K A] [EssFiniteType K A] [IsAlgClosed K] [IsLocalRing A] : IsField A

theorem Algebra.FormallyUnramified.isReduced_of_field (K : Type u_1) (A : Type u_2) [Field K] [CommRing A] [Algebra K A] [FormallyUnramified K A] [EssFiniteType K A] : IsReduced A

theorem Algebra.FormallyUnramified.isRadical_map_isMaximal (A : Type u_2) [CommRing A] (B : Type u_4) [CommRing B] [Algebra A B] [EssFiniteType A B] [FormallyUnramified A B] (p : Ideal A) [p.IsMaximal] : (Ideal.map (algebraMap A B) p).IsRadical

theorem Algebra.FormallyUnramified.range_eq_top_of_isPurelyInseparable (K : Type u_1) (L : Type u_3) [Field K] [Field L] [Algebra K L] [FormallyUnramified K L] [EssFiniteType K L] [IsPurelyInseparable K L] : (algebraMap K L).range = ⊤

theorem Algebra.FormallyUnramified.isSeparable (K : Type u_1) (L : Type u_3) [Field K] [Field L] [Algebra K L] [FormallyUnramified K L] [EssFiniteType K L] : Algebra.IsSeparable K L

theorem Algebra.FormallyUnramified.iff_isSeparable (K : Type u_1) [Field K] (L : Type u) [Field L] [Algebra K L] [EssFiniteType K L] : FormallyUnramified K L ↔ Algebra.IsSeparable K L

theorem Algebra.IsUnramifiedAt.not_minpoly_sq_dvd {K : Type u_1} {A : Type u_2} [Field K] [CommRing A] [Algebra K A] (Q : Ideal A) [Q.IsPrime] [IsUnramifiedAt K Q] (x : A) (p : Polynomial K) (hp₁ : Ideal.span {p} = RingHom.ker (Polynomial.aeval x).toRingHom) (hp₂ : Function.Surjective ⇑(Polynomial.aeval x)) : ¬minpoly K ((algebraMap A Q.ResidueField) x) ^ 2 ∣ p

If A = K[X]/⟨p⟩ is unramified at some prime Q, then the minpoly of X in κ(Q) only divides p once.