internlm/Lean-Github huggingface dataset:
Theorem: isUnramifiedAt_iff_SquareFree_minpoly
Proof state before:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁶ : CommRing R
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : IsDedekindDomain R
inst✝¹⁰ : Algebra R K
inst✝⁹ : IsFractionRing R K
inst✝⁸ : Algebra S L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra R L
inst✝⁵ : IsScalarTower R S L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsIntegralClosure S R L
inst✝² : FiniteDimensional K L
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDedekindDomain S
p : Ideal R
hp : p.IsPrime
hpbot : p ≠ ⊥
x : S
hx : Ideal.comap (algebraMap R S) (conductor R x) ⊔ p = ⊤
hx' : IsIntegral R x
⊢ IsUnramifiedAt S p ↔ Squarefree (Polynomial.map (Ideal.Quotient.mk p) (minpoly R x))
Tactic:
classical
have := hp.isMaximal hpbot
rw [isUnramifiedAt_iff_normalizedFactors_nodup p hpbot,
  KummerDedekind.normalizedFactors_ideal_map_eq_normalizedFactors_min_poly_mk_map
  this hpbot hx hx', Multiset.nodup_map_iff_of_injective, Multiset.nodup_attach,
  ← squarefree_iff_nodup_normalizedFactors (Polynomial.map_monic_ne_zero (minpoly.monic hx'))]
exact Subtype.val_injective.comp
  (KummerDedekind.normalizedFactorsMapEquivNormalizedFactorsMinPolyMk
    this hpbot hx hx').symm.injective
Proof state after:
no goals
Theorem: isUnramifiedAt_iff_SquareFree_minpoly
Proof state before:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁶ : CommRing R
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : IsDedekindDomain R
inst✝¹⁰ : Algebra R K
inst✝⁹ : IsFractionRing R K
inst✝⁸ : Algebra S L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra R L
inst✝⁵ : IsScalarTower R S L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsIntegralClosure S R L
inst✝² : FiniteDimensional K L
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDedekindDomain S
p : Ideal R
hp : p.IsPrime
hpbot : p ≠ ⊥
x : S
hx : Ideal.comap (algebraMap R S) (conductor R x) ⊔ p = ⊤
hx' : IsIntegral R x
⊢ IsUnramifiedAt S p ↔ Squarefree (Polynomial.map (Ideal.Quotient.mk p) (minpoly R x))
Tactic:
have := hp.isMaximal hpbot
Proof state after:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁶ : CommRing R
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : IsDedekindDomain R
inst✝¹⁰ : Algebra R K
inst✝⁹ : IsFractionRing R K
inst✝⁸ : Algebra S L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra R L
inst✝⁵ : IsScalarTower R S L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsIntegralClosure S R L
inst✝² : FiniteDimensional K L
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDedekindDomain S
p : Ideal R
hp : p.IsPrime
hpbot : p ≠ ⊥
x : S
hx : Ideal.comap (algebraMap R S) (conductor R x) ⊔ p = ⊤
hx' : IsIntegral R x
this : p.IsMaximal
⊢ IsUnramifiedAt S p ↔ Squarefree (Polynomial.map (Ideal.Quotient.mk p) (minpoly R x))
Theorem: isUnramifiedAt_iff_SquareFree_minpoly
Proof state before:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁶ : CommRing R
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : IsDedekindDomain R
inst✝¹⁰ : Algebra R K
inst✝⁹ : IsFractionRing R K
inst✝⁸ : Algebra S L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra R L
inst✝⁵ : IsScalarTower R S L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsIntegralClosure S R L
inst✝² : FiniteDimensional K L
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDedekindDomain S
p : Ideal R
hp : p.IsPrime
hpbot : p ≠ ⊥
x : S
hx : Ideal.comap (algebraMap R S) (conductor R x) ⊔ p = ⊤
hx' : IsIntegral R x
this : p.IsMaximal
⊢ IsUnramifiedAt S p ↔ Squarefree (Polynomial.map (Ideal.Quotient.mk p) (minpoly R x))
Tactic:
rw [isUnramifiedAt_iff_normalizedFactors_nodup p hpbot,
  KummerDedekind.normalizedFactors_ideal_map_eq_normalizedFactors_min_poly_mk_map
  this hpbot hx hx', Multiset.nodup_map_iff_of_injective, Multiset.nodup_attach,
  ← squarefree_iff_nodup_normalizedFactors (Polynomial.map_monic_ne_zero (minpoly.monic hx'))]
Proof state after:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁶ : CommRing R
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : IsDedekindDomain R
inst✝¹⁰ : Algebra R K
inst✝⁹ : IsFractionRing R K
inst✝⁸ : Algebra S L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra R L
inst✝⁵ : IsScalarTower R S L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsIntegralClosure S R L
inst✝² : FiniteDimensional K L
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDedekindDomain S
p : Ideal R
hp : p.IsPrime
hpbot : p ≠ ⊥
x : S
hx : Ideal.comap (algebraMap R S) (conductor R x) ⊔ p = ⊤
hx' : IsIntegral R x
this : p.IsMaximal
⊢ Function.Injective fun f =>
    ↑((KummerDedekind.normalizedFactorsMapEquivNormalizedFactorsMinPolyMk this hpbot hx hx').symm f)
Theorem: isUnramifiedAt_iff_SquareFree_minpoly
Proof state before:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁶ : CommRing R
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : IsDedekindDomain R
inst✝¹⁰ : Algebra R K
inst✝⁹ : IsFractionRing R K
inst✝⁸ : Algebra S L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra R L
inst✝⁵ : IsScalarTower R S L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsIntegralClosure S R L
inst✝² : FiniteDimensional K L
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDedekindDomain S
p : Ideal R
hp : p.IsPrime
hpbot : p ≠ ⊥
x : S
hx : Ideal.comap (algebraMap R S) (conductor R x) ⊔ p = ⊤
hx' : IsIntegral R x
this : p.IsMaximal
⊢ Function.Injective fun f =>
    ↑((KummerDedekind.normalizedFactorsMapEquivNormalizedFactorsMinPolyMk this hpbot hx hx').symm f)
Tactic:
exact Subtype.val_injective.comp
  (KummerDedekind.normalizedFactorsMapEquivNormalizedFactorsMinPolyMk
    this hpbot hx hx').symm.injective
Proof state after:
no goals
Theorem: isUnramifiedAt_iff_SquareFree_minpoly_powerBasis
Proof state before:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : IsDedekindDomain R
inst✝¹² : Algebra R K
inst✝¹¹ : IsFractionRing R K
inst✝¹⁰ : Algebra S L
inst✝⁹ : Algebra K L
inst✝⁸ : Algebra R L
inst✝⁷ : IsScalarTower R S L
inst✝⁶ : IsScalarTower R K L
inst✝⁵ : IsIntegralClosure S R L
inst✝⁴ : FiniteDimensional K L
inst✝³ : NoZeroSMulDivisors R S
inst✝² : IsDedekindDomain S
inst✝¹ : Algebra.IsIntegral R S
pb : PowerBasis R S
p : Ideal R
inst✝ : p.IsPrime
hpbot : p ≠ ⊥
⊢ IsUnramifiedAt S p ↔ Squarefree (Polynomial.map (Ideal.Quotient.mk p) (minpoly R pb.gen))
Tactic:
rw [isUnramifiedAt_iff_SquareFree_minpoly p hpbot pb.gen _ _]
Proof state after:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : IsDedekindDomain R
inst✝¹² : Algebra R K
inst✝¹¹ : IsFractionRing R K
inst✝¹⁰ : Algebra S L
inst✝⁹ : Algebra K L
inst✝⁸ : Algebra R L
inst✝⁷ : IsScalarTower R S L
inst✝⁶ : IsScalarTower R K L
inst✝⁵ : IsIntegralClosure S R L
inst✝⁴ : FiniteDimensional K L
inst✝³ : NoZeroSMulDivisors R S
inst✝² : IsDedekindDomain S
inst✝¹ : Algebra.IsIntegral R S
pb : PowerBasis R S
p : Ideal R
inst✝ : p.IsPrime
hpbot : p ≠ ⊥
⊢ Ideal.comap (algebraMap R S) (conductor R pb.gen) ⊔ p = ⊤

R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : IsDedekindDomain R
inst✝¹² : Algebra R K
inst✝¹¹ : IsFractionRing R K
inst✝¹⁰ : Algebra S L
inst✝⁹ : Algebra K L
inst✝⁸ : Algebra R L
inst✝⁷ : IsScalarTower R S L
inst✝⁶ : IsScalarTower R K L
inst✝⁵ : IsIntegralClosure S R L
inst✝⁴ : FiniteDimensional K L
inst✝³ : NoZeroSMulDivisors R S
inst✝² : IsDedekindDomain S
inst✝¹ : Algebra.IsIntegral R S
pb : PowerBasis R S
p : Ideal R
inst✝ : p.IsPrime
hpbot : p ≠ ⊥
⊢ IsIntegral R pb.gen
Theorem: isUnramifiedAt_iff_SquareFree_minpoly_powerBasis
Proof state before:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : IsDedekindDomain R
inst✝¹² : Algebra R K
inst✝¹¹ : IsFractionRing R K
inst✝¹⁰ : Algebra S L
inst✝⁹ : Algebra K L
inst✝⁸ : Algebra R L
inst✝⁷ : IsScalarTower R S L
inst✝⁶ : IsScalarTower R K L
inst✝⁵ : IsIntegralClosure S R L
inst✝⁴ : FiniteDimensional K L
inst✝³ : NoZeroSMulDivisors R S
inst✝² : IsDedekindDomain S
inst✝¹ : Algebra.IsIntegral R S
pb : PowerBasis R S
p : Ideal R
inst✝ : p.IsPrime
hpbot : p ≠ ⊥
⊢ Ideal.comap (algebraMap R S) (conductor R pb.gen) ⊔ p = ⊤

R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : IsDedekindDomain R
inst✝¹² : Algebra R K
inst✝¹¹ : IsFractionRing R K
inst✝¹⁰ : Algebra S L
inst✝⁹ : Algebra K L
inst✝⁸ : Algebra R L
inst✝⁷ : IsScalarTower R S L
inst✝⁶ : IsScalarTower R K L
inst✝⁵ : IsIntegralClosure S R L
inst✝⁴ : FiniteDimensional K L
inst✝³ : NoZeroSMulDivisors R S
inst✝² : IsDedekindDomain S
inst✝¹ : Algebra.IsIntegral R S
pb : PowerBasis R S
p : Ideal R
inst✝ : p.IsPrime
hpbot : p ≠ ⊥
⊢ IsIntegral R pb.gen
Tactic:
rw [conductor_eq_top_of_powerBasis, Ideal.comap_top, top_sup_eq]
Proof state after:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : IsDedekindDomain R
inst✝¹² : Algebra R K
inst✝¹¹ : IsFractionRing R K
inst✝¹⁰ : Algebra S L
inst✝⁹ : Algebra K L
inst✝⁸ : Algebra R L
inst✝⁷ : IsScalarTower R S L
inst✝⁶ : IsScalarTower R K L
inst✝⁵ : IsIntegralClosure S R L
inst✝⁴ : FiniteDimensional K L
inst✝³ : NoZeroSMulDivisors R S
inst✝² : IsDedekindDomain S
inst✝¹ : Algebra.IsIntegral R S
pb : PowerBasis R S
p : Ideal R
inst✝ : p.IsPrime
hpbot : p ≠ ⊥
⊢ IsIntegral R pb.gen
Theorem: isUnramifiedAt_iff_SquareFree_minpoly_powerBasis
Proof state before:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : IsDedekindDomain R
inst✝¹² : Algebra R K
inst✝¹¹ : IsFractionRing R K
inst✝¹⁰ : Algebra S L
inst✝⁹ : Algebra K L
inst✝⁸ : Algebra R L
inst✝⁷ : IsScalarTower R S L
inst✝⁶ : IsScalarTower R K L
inst✝⁵ : IsIntegralClosure S R L
inst✝⁴ : FiniteDimensional K L
inst✝³ : NoZeroSMulDivisors R S
inst✝² : IsDedekindDomain S
inst✝¹ : Algebra.IsIntegral R S
pb : PowerBasis R S
p : Ideal R
inst✝ : p.IsPrime
hpbot : p ≠ ⊥
⊢ IsIntegral R pb.gen
Tactic:
exact PowerBasis.isIntegral_gen pb
Proof state after:
no goals
Theorem: isUnramifiedAt_of_Separable_minpoly'
Proof state before:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Algebra S L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R S L
inst✝³ : IsScalarTower R K L
inst✝² : IsIntegralClosure S R L
inst✝¹ : FiniteDimensional K L
inst✝ : IsSeparable K L
p : Ideal R
hp : p.IsPrime
hpbot : p ≠ ⊥
x : S
hx' : Algebra.adjoin K {(algebraMap S L) x} = ⊤
h : (map (Ideal.Quotient.mk p) (minpoly R x)).Separable
⊢ IsUnramifiedAt S p
Tactic:
have : IsDomain S :=
  (IsIntegralClosure.equiv R S L (integralClosure R L)).toMulEquiv.isDomain (integralClosure R L)
Proof state after:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Algebra S L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R S L
inst✝³ : IsScalarTower R K L
inst✝² : IsIntegralClosure S R L
inst✝¹ : FiniteDimensional K L
inst✝ : IsSeparable K L
p : Ideal R
hp : p.IsPrime
hpbot : p ≠ ⊥
x : S
hx' : Algebra.adjoin K {(algebraMap S L) x} = ⊤
h : (map (Ideal.Quotient.mk p) (minpoly R x)).Separable
this : IsDomain S
⊢ IsUnramifiedAt S p
Theorem: isUnramifiedAt_of_Separable_minpoly'
Proof state before:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Algebra S L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R S L
inst✝³ : IsScalarTower R K L
inst✝² : IsIntegralClosure S R L
inst✝¹ : FiniteDimensional K L
inst✝ : IsSeparable K L
p : Ideal R
hp : p.IsPrime
hpbot : p ≠ ⊥
x : S
hx' : Algebra.adjoin K {(algebraMap S L) x} = ⊤
h : (map (Ideal.Quotient.mk p) (minpoly R x)).Separable
this : IsDomain S
⊢ IsUnramifiedAt S p
Tactic:
have hRS : Function.Injective (algebraMap R S) := by
  refine Function.Injective.of_comp (f := algebraMap S L) ?_
  rw [← RingHom.coe_comp, ← IsScalarTower.algebraMap_eq, IsScalarTower.algebraMap_eq R K L]
  exact (algebraMap K L).injective.comp (IsFractionRing.injective _ _)
Proof state after:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Algebra S L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R S L
inst✝³ : IsScalarTower R K L
inst✝² : IsIntegralClosure S R L
inst✝¹ : FiniteDimensional K L
inst✝ : IsSeparable K L
p : Ideal R
hp : p.IsPrime
hpbot : p ≠ ⊥
x : S
hx' : Algebra.adjoin K {(algebraMap S L) x} = ⊤
h : (map (Ideal.Quotient.mk p) (minpoly R x)).Separable
this : IsDomain S
hRS : Function.Injective ⇑(algebraMap R S)
⊢ IsUnramifiedAt S p
Theorem: isUnramifiedAt_of_Separable_minpoly'
Proof state before:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Algebra S L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R S L
inst✝³ : IsScalarTower R K L
inst✝² : IsIntegralClosure S R L
inst✝¹ : FiniteDimensional K L
inst✝ : IsSeparable K L
p : Ideal R
hp : p.IsPrime
hpbot : p ≠ ⊥
x : S
hx' : Algebra.adjoin K {(algebraMap S L) x} = ⊤
h : (map (Ideal.Quotient.mk p) (minpoly R x)).Separable
this : IsDomain S
hRS : Function.Injective ⇑(algebraMap R S)
⊢ IsUnramifiedAt S p
Tactic:
have := NoZeroSMulDivisors.iff_algebraMap_injective.mpr hRS
Proof state after:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Algebra S L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R S L
inst✝³ : IsScalarTower R K L
inst✝² : IsIntegralClosure S R L
inst✝¹ : FiniteDimensional K L
inst✝ : IsSeparable K L
p : Ideal R
hp : p.IsPrime
hpbot : p ≠ ⊥
x : S
hx' : Algebra.adjoin K {(algebraMap S L) x} = ⊤
h : (map (Ideal.Quotient.mk p) (minpoly R x)).Separable
this✝ : IsDomain S
hRS : Function.Injective ⇑(algebraMap R S)
this : NoZeroSMulDivisors R S
⊢ IsUnramifiedAt S p
Theorem: isUnramifiedAt_of_Separable_minpoly'
Proof state before:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Algebra S L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R S L
inst✝³ : IsScalarTower R K L
inst✝² : IsIntegralClosure S R L
inst✝¹ : FiniteDimensional K L
inst✝ : IsSeparable K L
p : Ideal R
hp : p.IsPrime
hpbot : p ≠ ⊥
x : S
hx' : Algebra.adjoin K {(algebraMap S L) x} = ⊤
h : (map (Ideal.Quotient.mk p) (minpoly R x)).Separable
this✝ : IsDomain S
hRS : Function.Injective ⇑(algebraMap R S)
this : NoZeroSMulDivisors R S
⊢ IsUnramifiedAt S p
Tactic:
have := IsIntegralClosure.isNoetherian R K L S
Proof state after:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Algebra S L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R S L
inst✝³ : IsScalarTower R K L
inst✝² : IsIntegralClosure S R L
inst✝¹ : FiniteDimensional K L
inst✝ : IsSeparable K L
p : Ideal R
hp : p.IsPrime
hpbot : p ≠ ⊥
x : S
hx' : Algebra.adjoin K {(algebraMap S L) x} = ⊤
h : (map (Ideal.Quotient.mk p) (minpoly R x)).Separable
this✝¹ : IsDomain S
hRS : Function.Injective ⇑(algebraMap R S)
this✝ : NoZeroSMulDivisors R S
this : IsNoetherian R S
⊢ IsUnramifiedAt S p
Theorem: isUnramifiedAt_of_Separable_minpoly'
Proof state before:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Algebra S L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R S L
inst✝³ : IsScalarTower R K L
inst✝² : IsIntegralClosure S R L
inst✝¹ : FiniteDimensional K L
inst✝ : IsSeparable K L
p : Ideal R
hp : p.IsPrime
hpbot : p ≠ ⊥
x : S
hx' : Algebra.adjoin K {(algebraMap S L) x} = ⊤
h : (map (Ideal.Quotient.mk p) (minpoly R x)).Separable
this✝¹ : IsDomain S
hRS : Function.Injective ⇑(algebraMap R S)
this✝ : NoZeroSMulDivisors R S
this : IsNoetherian R S
⊢ IsUnramifiedAt S p
Tactic:
have := IsIntegralClosure.isDedekindDomain R K L S
Proof state after:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Algebra S L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R S L
inst✝³ : IsScalarTower R K L
inst✝² : IsIntegralClosure S R L
inst✝¹ : FiniteDimensional K L
inst✝ : IsSeparable K L
p : Ideal R
hp : p.IsPrime
hpbot : p ≠ ⊥
x : S
hx' : Algebra.adjoin K {(algebraMap S L) x} = ⊤
h : (map (Ideal.Quotient.mk p) (minpoly R x)).Separable
this✝² : IsDomain S
hRS : Function.Injective ⇑(algebraMap R S)
this✝¹ : NoZeroSMulDivisors R S
this✝ : IsNoetherian R S
this : IsDedekindDomain S
⊢ IsUnramifiedAt S p
Theorem: isUnramifiedAt_of_Separable_minpoly'
Proof state before:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Algebra S L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R S L
inst✝³ : IsScalarTower R K L
inst✝² : IsIntegralClosure S R L
inst✝¹ : FiniteDimensional K L
inst✝ : IsSeparable K L
p : Ideal R
hp : p.IsPrime
hpbot : p ≠ ⊥
x : S
hx' : Algebra.adjoin K {(algebraMap S L) x} = ⊤
h : (map (Ideal.Quotient.mk p) (minpoly R x)).Separable
this✝² : IsDomain S
hRS : Function.Injective ⇑(algebraMap R S)
this✝¹ : NoZeroSMulDivisors R S
this✝ : IsNoetherian R S
this : IsDedekindDomain S
⊢ IsUnramifiedAt S p
Tactic:
have := IsIntegralClosure.isFractionRing_of_finite_extension R K L S
Proof state after:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Algebra S L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R S L
inst✝³ : IsScalarTower R K L
inst✝² : IsIntegralClosure S R L
inst✝¹ : FiniteDimensional K L
inst✝ : IsSeparable K L
p : Ideal R
hp : p.IsPrime
hpbot : p ≠ ⊥
x : S
hx' : Algebra.adjoin K {(algebraMap S L) x} = ⊤
h : (map (Ideal.Quotient.mk p) (minpoly R x)).Separable
this✝³ : IsDomain S
hRS : Function.Injective ⇑(algebraMap R S)
this✝² : NoZeroSMulDivisors R S
this✝¹ : IsNoetherian R S
this✝ : IsDedekindDomain S
this : IsFractionRing S L
⊢ IsUnramifiedAt S p
Theorem: isUnramifiedAt_of_Separable_minpoly'
Proof state before:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Algebra S L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R S L
inst✝³ : IsScalarTower R K L
inst✝² : IsIntegralClosure S R L
inst✝¹ : FiniteDimensional K L
inst✝ : IsSeparable K L
p : Ideal R
hp : p.IsPrime
hpbot : p ≠ ⊥
x : S
hx' : Algebra.adjoin K {(algebraMap S L) x} = ⊤
h : (map (Ideal.Quotient.mk p) (minpoly R x)).Separable
this✝³ : IsDomain S
hRS : Function.Injective ⇑(algebraMap R S)
this✝² : NoZeroSMulDivisors R S
this✝¹ : IsNoetherian R S
this✝ : IsDedekindDomain S
this : IsFractionRing S L
⊢ IsUnramifiedAt S p
Tactic:
have := aeval_derivative_mem_differentIdeal R K L x hx'
Proof state after:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Algebra S L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R S L
inst✝³ : IsScalarTower R K L
inst✝² : IsIntegralClosure S R L
inst✝¹ : FiniteDimensional K L
inst✝ : IsSeparable K L
p : Ideal R
hp : p.IsPrime
hpbot : p ≠ ⊥
x : S
hx' : Algebra.adjoin K {(algebraMap S L) x} = ⊤
h : (map (Ideal.Quotient.mk p) (minpoly R x)).Separable
this✝⁴ : IsDomain S
hRS : Function.Injective ⇑(algebraMap R S)
this✝³ : NoZeroSMulDivisors R S
this✝² : IsNoetherian R S
this✝¹ : IsDedekindDomain S
this✝ : IsFractionRing S L
this : (aeval x) (derivative (minpoly R x)) ∈ differentIdeal R S
⊢ IsUnramifiedAt S p
Theorem: isUnramifiedAt_of_Separable_minpoly'
Proof state before:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Algebra S L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R S L
inst✝³ : IsScalarTower R K L
inst✝² : IsIntegralClosure S R L
inst✝¹ : FiniteDimensional K L
inst✝ : IsSeparable K L
p : Ideal R
hp : p.IsPrime
hpbot : p ≠ ⊥
x : S
hx' : Algebra.adjoin K {(algebraMap S L) x} = ⊤
h : (map (Ideal.Quotient.mk p) (minpoly R x)).Separable
this✝⁴ : IsDomain S
hRS : Function.Injective ⇑(algebraMap R S)
this✝³ : NoZeroSMulDivisors R S
this✝² : IsNoetherian R S
this✝¹ : IsDedekindDomain S
this✝ : IsFractionRing S L
this : (aeval x) (derivative (minpoly R x)) ∈ differentIdeal R S
⊢ IsUnramifiedAt S p
Tactic:
have H : RingHom.comp (algebraMap (FractionRing R) (FractionRing S))
  ↑(FractionRing.algEquiv R K).symm.toRingEquiv =
    RingHom.comp ↑(FractionRing.algEquiv S L).symm.toRingEquiv (algebraMap K L) := by
  apply IsLocalization.ringHom_ext R⁰
  ext
  simp only [AlgEquiv.toRingEquiv_eq_coe, RingHom.coe_comp, RingHom.coe_coe,
    AlgEquiv.coe_ringEquiv, Function.comp_apply, AlgEquiv.commutes,
    ← IsScalarTower.algebraMap_apply]
  rw [IsScalarTower.algebraMap_apply R S L, AlgEquiv.commutes, ← IsScalarTower.algebraMap_apply]
Proof state after:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Algebra S L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R S L
inst✝³ : IsScalarTower R K L
inst✝² : IsIntegralClosure S R L
inst✝¹ : FiniteDimensional K L
inst✝ : IsSeparable K L
p : Ideal R
hp : p.IsPrime
hpbot : p ≠ ⊥
x : S
hx' : Algebra.adjoin K {(algebraMap S L) x} = ⊤
h : (map (Ideal.Quotient.mk p) (minpoly R x)).Separable
this✝⁴ : IsDomain S
hRS : Function.Injective ⇑(algebraMap R S)
this✝³ : NoZeroSMulDivisors R S
this✝² : IsNoetherian R S
this✝¹ : IsDedekindDomain S
this✝ : IsFractionRing S L
this : (aeval x) (derivative (minpoly R x)) ∈ differentIdeal R S
H :
  (algebraMap (FractionRing R) (FractionRing S)).comp ↑(FractionRing.algEquiv R K).symm.toRingEquiv =
    (↑(FractionRing.algEquiv S L).symm.toRingEquiv).comp (algebraMap K L)
⊢ IsUnramifiedAt S p