Theorem: isUnramifiedAt_iff_SquareFree_minpoly (FltRegular/NumberTheory/Unramified.lean)

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
State after:
no goals

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
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))

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'))]
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)

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
State after:
no goals