Unramified extensions

Main results

• comap_map_eq_of_unramified: If K/L is galois, S/R is unramified, then any ideal I fixed by Gal(L/K) satisfies (I ∩ R)S = I.
• isUnramifiedAt_of_Separable_minpoly: If L = K[α] with α integral over R, and f'(α) mod p is separable for the prime below P, then S/R is unramified at P.

theorem algebraMap_injective_of_isIntegralClosure {R : Type u_1} (K : Type u_2) (L : Type u_3) {S : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [Field K] [Field L] [Algebra R K] [IsFractionRing R K] [Algebra S L] [Algebra K L] [Algebra R L] [IsScalarTower R S L] [IsScalarTower R K L] : Function.Injective ⇑(algebraMap R S)

In the AKLB setup, the map from R to the integral closure S of R in L is injective.

theorem comap_map_eq_of_unramified {R : Type u_1} (K : Type u_2) (L : Type u_3) {S : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [Field K] [Field L] [IsDedekindDomain R] [Algebra R K] [IsFractionRing R K] [Algebra S L] [Algebra K L] [Algebra R L] [IsScalarTower R S L] [IsScalarTower R K L] [IsIntegralClosure S R L] [FiniteDimensional K L] [IsGalois K L] [Algebra.Unramified R S] (I : Ideal S) (hI : ∀ (σ : Gal(L/K)), Ideal.comap ((galRestrict R K L S) σ) I = I) : Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) I) = I

theorem isUnramifiedAt_of_Separable_minpoly' {R : Type u_1} (K : Type u_2) (L : Type u_3) {S : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [Field K] [Field L] [IsDedekindDomain R] [Algebra R K] [IsFractionRing R K] [Algebra S L] [Algebra K L] [Algebra R L] [IsScalarTower R S L] [IsScalarTower R K L] [IsIntegralClosure S R L] [FiniteDimensional K L] [Algebra.IsSeparable K L] (P : Ideal S) [hP : P.IsPrime] (hPbot : P ≠ ⊥) (x : S) (hx' : K[(algebraMap S L) x] = ⊤) (h : (Polynomial.map (Ideal.Quotient.mk (Ideal.under R P)) (minpoly R x)).Separable) : Algebra.IsUnramifiedAt R P

theorem isUnramifiedAt_of_Separable_minpoly {R : Type u_1} (K : Type u_2) (L : Type u_3) {S : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [Field K] [Field L] [IsDedekindDomain R] [Algebra R K] [IsFractionRing R K] [Algebra S L] [Algebra K L] [Algebra R L] [IsScalarTower R S L] [IsScalarTower R K L] [IsIntegralClosure S R L] [FiniteDimensional K L] [Algebra.IsSeparable K L] (P : Ideal S) [hP : P.IsPrime] (hPbot : P ≠ ⊥) (x : L) (hx : IsIntegral R x) (hx' : K[x] = ⊤) (h : (Polynomial.map (Ideal.Quotient.mk (Ideal.under R P)) (minpoly R x)).Separable) : Algebra.IsUnramifiedAt R P