internlm/Lean-Github huggingface dataset:
Theorem: comap_map_eq_of_isUnramified
Proof state before:
case neg.a.e_a
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✝¹ : IsGalois K L
inst✝ : IsUnramified R S
I : Ideal S
hI : ∀ (σ : L ≃ₐ[K] L), Ideal.comap ((galRestrict R K L S) σ) I = I
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
hRS : Function.Injective ⇑(algebraMap R S)
this✝ : NoZeroSMulDivisors R S
hIbot : ¬I = ⊥
h1 : Algebra.IsIntegral R S
hIbot' : Ideal.comap (algebraMap R S) I ≠ ⊥
𝔓 : (p : Ideal R) → p.IsPrime ∧ Ideal.comap (algebraMap R S) I ≤ p → Ideal S
h𝔓 : ∀ (p : Ideal R) (a : p.IsPrime ∧ Ideal.comap (algebraMap R S) I ≤ p), 𝔓 p a ≥ I
h𝔓' : ∀ (p : Ideal R) (a : p.IsPrime ∧ Ideal.comap (algebraMap R S) I ≤ p), 𝔓 p a ∈ primesOver S p
p : Ideal R
hp : p.IsPrime ∧ Ideal.comap (algebraMap R S) I ≤ p
hpbot : p ≠ ⊥
hpbot' : Ideal.map (algebraMap R S) p ≠ ⊥
this : p.IsPrime
P : Ideal S
hP : P ∈ primesOver S p
n : ℕ
σ : L ≃ₐ[K] L
hσ : Ideal.comap ((galRestrict R K L S) σ) (𝔓 p hp) = P
⊢ P ^ n ∣ I ↔ 𝔓 p hp ^ n ∣ I
Tactic:
rw [Ideal.dvd_iff_le, Ideal.dvd_iff_le]
Proof state after:
case neg.a.e_a
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✝¹ : IsGalois K L
inst✝ : IsUnramified R S
I : Ideal S
hI : ∀ (σ : L ≃ₐ[K] L), Ideal.comap ((galRestrict R K L S) σ) I = I
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
hRS : Function.Injective ⇑(algebraMap R S)
this✝ : NoZeroSMulDivisors R S
hIbot : ¬I = ⊥
h1 : Algebra.IsIntegral R S
hIbot' : Ideal.comap (algebraMap R S) I ≠ ⊥
𝔓 : (p : Ideal R) → p.IsPrime ∧ Ideal.comap (algebraMap R S) I ≤ p → Ideal S
h𝔓 : ∀ (p : Ideal R) (a : p.IsPrime ∧ Ideal.comap (algebraMap R S) I ≤ p), 𝔓 p a ≥ I
h𝔓' : ∀ (p : Ideal R) (a : p.IsPrime ∧ Ideal.comap (algebraMap R S) I ≤ p), 𝔓 p a ∈ primesOver S p
p : Ideal R
hp : p.IsPrime ∧ Ideal.comap (algebraMap R S) I ≤ p
hpbot : p ≠ ⊥
hpbot' : Ideal.map (algebraMap R S) p ≠ ⊥
this : p.IsPrime
P : Ideal S
hP : P ∈ primesOver S p
n : ℕ
σ : L ≃ₐ[K] L
hσ : Ideal.comap ((galRestrict R K L S) σ) (𝔓 p hp) = P
⊢ I ≤ P ^ n ↔ I ≤ 𝔓 p hp ^ n
Theorem: comap_map_eq_of_isUnramified
Proof state before:
case neg.a.e_a
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✝¹ : IsGalois K L
inst✝ : IsUnramified R S
I : Ideal S
hI : ∀ (σ : L ≃ₐ[K] L), Ideal.comap ((galRestrict R K L S) σ) I = I
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
hRS : Function.Injective ⇑(algebraMap R S)
this✝ : NoZeroSMulDivisors R S
hIbot : ¬I = ⊥
h1 : Algebra.IsIntegral R S
hIbot' : Ideal.comap (algebraMap R S) I ≠ ⊥
𝔓 : (p : Ideal R) → p.IsPrime ∧ Ideal.comap (algebraMap R S) I ≤ p → Ideal S
h𝔓 : ∀ (p : Ideal R) (a : p.IsPrime ∧ Ideal.comap (algebraMap R S) I ≤ p), 𝔓 p a ≥ I
h𝔓' : ∀ (p : Ideal R) (a : p.IsPrime ∧ Ideal.comap (algebraMap R S) I ≤ p), 𝔓 p a ∈ primesOver S p
p : Ideal R
hp : p.IsPrime ∧ Ideal.comap (algebraMap R S) I ≤ p
hpbot : p ≠ ⊥
hpbot' : Ideal.map (algebraMap R S) p ≠ ⊥
this : p.IsPrime
P : Ideal S
hP : P ∈ primesOver S p
n : ℕ
σ : L ≃ₐ[K] L
hσ : Ideal.comap ((galRestrict R K L S) σ) (𝔓 p hp) = P
⊢ I ≤ P ^ n ↔ I ≤ 𝔓 p hp ^ n
Tactic:
conv_lhs => rw [← hI σ, ← hσ,
  Ideal.comap_le_iff_le_map _ (AlgEquiv.bijective _), Ideal.map_pow,
  Ideal.map_comap_of_surjective _ (AlgEquiv.surjective _)]
Proof state after:
no goals
Theorem: comap_map_eq_of_isUnramified
Proof state before:
case neg.h
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✝¹ : IsGalois K L
inst✝ : IsUnramified R S
I : Ideal S
hI : ∀ (σ : L ≃ₐ[K] L), Ideal.comap ((galRestrict R K L S) σ) I = I
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : Function.Injective ⇑(algebraMap R S)
this : NoZeroSMulDivisors R S
hIbot : ¬I = ⊥
h1 : Algebra.IsIntegral R S
hIbot' : Ideal.comap (algebraMap R S) I ≠ ⊥
𝔓 : (p : Ideal R) → p.IsPrime ∧ Ideal.comap (algebraMap R S) I ≤ p → Ideal S
h𝔓 : ∀ (p : Ideal R) (a : p.IsPrime ∧ Ideal.comap (algebraMap R S) I ≤ p), 𝔓 p a ≥ I
h𝔓' : ∀ (p : Ideal R) (a : p.IsPrime ∧ Ideal.comap (algebraMap R S) I ≤ p), 𝔓 p a ∈ primesOver S p
⊢ ∀ i ∈ (factors I).toFinset, Ideal.comap (algebraMap R S) i ∈ (factors (Ideal.comap (algebraMap R S) I)).toFinset
Tactic:
intro P hP
Proof state after:
case neg.h
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✝¹ : IsGalois K L
inst✝ : IsUnramified R S
I : Ideal S
hI : ∀ (σ : L ≃ₐ[K] L), Ideal.comap ((galRestrict R K L S) σ) I = I
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : Function.Injective ⇑(algebraMap R S)
this : NoZeroSMulDivisors R S
hIbot : ¬I = ⊥
h1 : Algebra.IsIntegral R S
hIbot' : Ideal.comap (algebraMap R S) I ≠ ⊥
𝔓 : (p : Ideal R) → p.IsPrime ∧ Ideal.comap (algebraMap R S) I ≤ p → Ideal S
h𝔓 : ∀ (p : Ideal R) (a : p.IsPrime ∧ Ideal.comap (algebraMap R S) I ≤ p), 𝔓 p a ≥ I
h𝔓' : ∀ (p : Ideal R) (a : p.IsPrime ∧ Ideal.comap (algebraMap R S) I ≤ p), 𝔓 p a ∈ primesOver S p
P : Ideal S
hP : P ∈ (factors I).toFinset
⊢ Ideal.comap (algebraMap R S) P ∈ (factors (Ideal.comap (algebraMap R S) I)).toFinset
Theorem: comap_map_eq_of_isUnramified
Proof state before:
case neg.h
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✝¹ : IsGalois K L
inst✝ : IsUnramified R S
I : Ideal S
hI : ∀ (σ : L ≃ₐ[K] L), Ideal.comap ((galRestrict R K L S) σ) I = I
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : Function.Injective ⇑(algebraMap R S)
this : NoZeroSMulDivisors R S
hIbot : ¬I = ⊥
h1 : Algebra.IsIntegral R S
hIbot' : Ideal.comap (algebraMap R S) I ≠ ⊥
𝔓 : (p : Ideal R) → p.IsPrime ∧ Ideal.comap (algebraMap R S) I ≤ p → Ideal S
h𝔓 : ∀ (p : Ideal R) (a : p.IsPrime ∧ Ideal.comap (algebraMap R S) I ≤ p), 𝔓 p a ≥ I
h𝔓' : ∀ (p : Ideal R) (a : p.IsPrime ∧ Ideal.comap (algebraMap R S) I ≤ p), 𝔓 p a ∈ primesOver S p
P : Ideal S
hP : P ∈ (factors I).toFinset
⊢ Ideal.comap (algebraMap R S) P ∈ (factors (Ideal.comap (algebraMap R S) I)).toFinset
Tactic:
simp only [factors_eq_normalizedFactors, Multiset.mem_toFinset,
  Ideal.mem_normalizedFactors_iff hIbot] at hP
Proof state after:
case neg.h
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✝¹ : IsGalois K L
inst✝ : IsUnramified R S
I : Ideal S
hI : ∀ (σ : L ≃ₐ[K] L), Ideal.comap ((galRestrict R K L S) σ) I = I
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : Function.Injective ⇑(algebraMap R S)
this : NoZeroSMulDivisors R S
hIbot : ¬I = ⊥
h1 : Algebra.IsIntegral R S
hIbot' : Ideal.comap (algebraMap R S) I ≠ ⊥
𝔓 : (p : Ideal R) → p.IsPrime ∧ Ideal.comap (algebraMap R S) I ≤ p → Ideal S
h𝔓 : ∀ (p : Ideal R) (a : p.IsPrime ∧ Ideal.comap (algebraMap R S) I ≤ p), 𝔓 p a ≥ I
h𝔓' : ∀ (p : Ideal R) (a : p.IsPrime ∧ Ideal.comap (algebraMap R S) I ≤ p), 𝔓 p a ∈ primesOver S p
P : Ideal S
hP : P.IsPrime ∧ I ≤ P
⊢ Ideal.comap (algebraMap R S) P ∈ (factors (Ideal.comap (algebraMap R S) I)).toFinset
Theorem: comap_map_eq_of_isUnramified
Proof state before:
case neg.h
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✝¹ : IsGalois K L
inst✝ : IsUnramified R S
I : Ideal S
hI : ∀ (σ : L ≃ₐ[K] L), Ideal.comap ((galRestrict R K L S) σ) I = I
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : Function.Injective ⇑(algebraMap R S)
this : NoZeroSMulDivisors R S
hIbot : ¬I = ⊥
h1 : Algebra.IsIntegral R S
hIbot' : Ideal.comap (algebraMap R S) I ≠ ⊥
𝔓 : (p : Ideal R) → p.IsPrime ∧ Ideal.comap (algebraMap R S) I ≤ p → Ideal S
h𝔓 : ∀ (p : Ideal R) (a : p.IsPrime ∧ Ideal.comap (algebraMap R S) I ≤ p), 𝔓 p a ≥ I
h𝔓' : ∀ (p : Ideal R) (a : p.IsPrime ∧ Ideal.comap (algebraMap R S) I ≤ p), 𝔓 p a ∈ primesOver S p
P : Ideal S
hP : P.IsPrime ∧ I ≤ P
⊢ Ideal.comap (algebraMap R S) P ∈ (factors (Ideal.comap (algebraMap R S) I)).toFinset
Tactic:
simp only [factors_eq_normalizedFactors, Multiset.mem_toFinset,
  Ideal.mem_normalizedFactors_iff hIbot']
Proof state after:
case neg.h
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✝¹ : IsGalois K L
inst✝ : IsUnramified R S
I : Ideal S
hI : ∀ (σ : L ≃ₐ[K] L), Ideal.comap ((galRestrict R K L S) σ) I = I
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : Function.Injective ⇑(algebraMap R S)
this : NoZeroSMulDivisors R S
hIbot : ¬I = ⊥
h1 : Algebra.IsIntegral R S
hIbot' : Ideal.comap (algebraMap R S) I ≠ ⊥
𝔓 : (p : Ideal R) → p.IsPrime ∧ Ideal.comap (algebraMap R S) I ≤ p → Ideal S
h𝔓 : ∀ (p : Ideal R) (a : p.IsPrime ∧ Ideal.comap (algebraMap R S) I ≤ p), 𝔓 p a ≥ I
h𝔓' : ∀ (p : Ideal R) (a : p.IsPrime ∧ Ideal.comap (algebraMap R S) I ≤ p), 𝔓 p a ∈ primesOver S p
P : Ideal S
hP : P.IsPrime ∧ I ≤ P
⊢ (Ideal.comap (algebraMap R S) P).IsPrime ∧ Ideal.comap (algebraMap R S) I ≤ Ideal.comap (algebraMap R S) P
Theorem: comap_map_eq_of_isUnramified
Proof state before:
case neg.h
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✝¹ : IsGalois K L
inst✝ : IsUnramified R S
I : Ideal S
hI : ∀ (σ : L ≃ₐ[K] L), Ideal.comap ((galRestrict R K L S) σ) I = I
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : Function.Injective ⇑(algebraMap R S)
this : NoZeroSMulDivisors R S
hIbot : ¬I = ⊥
h1 : Algebra.IsIntegral R S
hIbot' : Ideal.comap (algebraMap R S) I ≠ ⊥
𝔓 : (p : Ideal R) → p.IsPrime ∧ Ideal.comap (algebraMap R S) I ≤ p → Ideal S
h𝔓 : ∀ (p : Ideal R) (a : p.IsPrime ∧ Ideal.comap (algebraMap R S) I ≤ p), 𝔓 p a ≥ I
h𝔓' : ∀ (p : Ideal R) (a : p.IsPrime ∧ Ideal.comap (algebraMap R S) I ≤ p), 𝔓 p a ∈ primesOver S p
P : Ideal S
hP : P.IsPrime ∧ I ≤ P
⊢ (Ideal.comap (algebraMap R S) P).IsPrime ∧ Ideal.comap (algebraMap R S) I ≤ Ideal.comap (algebraMap R S) P
Tactic:
exact ⟨hP.1.comap _, Ideal.comap_mono hP.2⟩
Proof state after:
no goals
Theorem: isUnramifiedAt_iff_normalizedFactors_nodup
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
inst✝ : p.IsPrime
hp : p ≠ ⊥
⊢ IsUnramifiedAt S p ↔ (normalizedFactors (Ideal.map (algebraMap R S) p)).Nodup
Tactic:
simp_rw [Multiset.nodup_iff_count_eq_one, ← Multiset.mem_toFinset,
  ← factors_eq_normalizedFactors]
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
inst✝ : p.IsPrime
hp : p ≠ ⊥
⊢ IsUnramifiedAt S p ↔
    ∀ a ∈ (factors (Ideal.map (algebraMap R S) p)).toFinset,
      Multiset.count a (factors (Ideal.map (algebraMap R S) p)) = 1
Theorem: isUnramifiedAt_iff_normalizedFactors_nodup
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
inst✝ : p.IsPrime
hp : p ≠ ⊥
⊢ IsUnramifiedAt S p ↔
    ∀ a ∈ (factors (Ideal.map (algebraMap R S) p)).toFinset,
      Multiset.count a (factors (Ideal.map (algebraMap R S) p)) = 1
Tactic:
show _ ↔ ∀ P ∈ (primesOverFinset S p : Set (Ideal 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✝² : NoZeroSMulDivisors R S
inst✝¹ : IsDedekindDomain S
p : Ideal R
inst✝ : p.IsPrime
hp : p ≠ ⊥
⊢ IsUnramifiedAt S p ↔ ∀ P ∈ ↑(primesOverFinset S p), Multiset.count P (factors (Ideal.map (algebraMap R S) p)) = 1
Theorem: isUnramifiedAt_iff_normalizedFactors_nodup
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
inst✝ : p.IsPrime
hp : p ≠ ⊥
⊢ IsUnramifiedAt S p ↔ ∀ P ∈ ↑(primesOverFinset S p), Multiset.count P (factors (Ideal.map (algebraMap R S) p)) = 1
Tactic:
simp_rw [IsUnramifiedAt, coe_primesOverFinset S p hp]
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
inst✝ : p.IsPrime
hp : p ≠ ⊥
⊢ (∀ P ∈ primesOver S p, Ideal.ramificationIdx (algebraMap R S) p P = 1) ↔
    ∀ P ∈ primesOver S p, Multiset.count P (factors (Ideal.map (algebraMap R S) p)) = 1
Theorem: isUnramifiedAt_iff_normalizedFactors_nodup
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
inst✝ : p.IsPrime
hp : p ≠ ⊥
⊢ (∀ P ∈ primesOver S p, Ideal.ramificationIdx (algebraMap R S) p P = 1) ↔
    ∀ P ∈ primesOver S p, Multiset.count P (factors (Ideal.map (algebraMap R S) p)) = 1
Tactic:
refine forall₂_congr (fun P hP ↦ ?_)
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
inst✝ : p.IsPrime
hp : p ≠ ⊥
P : Ideal S
hP : P ∈ primesOver S p
⊢ Ideal.ramificationIdx (algebraMap R S) p P = 1 ↔ Multiset.count P (factors (Ideal.map (algebraMap R S) p)) = 1
Theorem: isUnramifiedAt_iff_normalizedFactors_nodup
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
inst✝ : p.IsPrime
hp : p ≠ ⊥
P : Ideal S
hP : P ∈ primesOver S p
⊢ Ideal.ramificationIdx (algebraMap R S) p P = 1 ↔ Multiset.count P (factors (Ideal.map (algebraMap R S) p)) = 1
Tactic:
rw [Ideal.IsDedekindDomain.ramificationIdx_eq_factors_count]
Proof state after:
case hp0
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
inst✝ : p.IsPrime
hp : p ≠ ⊥
P : Ideal S
hP : P ∈ primesOver S p
⊢ Ideal.map (algebraMap R S) p ≠ ⊥

case hP
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
inst✝ : p.IsPrime
hp : p ≠ ⊥
P : Ideal S
hP : P ∈ primesOver S p
⊢ P.IsPrime

case hP0
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
inst✝ : p.IsPrime
hp : p ≠ ⊥
P : Ideal S
hP : P ∈ primesOver S p
⊢ P ≠ ⊥
Theorem: isUnramifiedAt_iff_normalizedFactors_nodup
Proof state before:
case hp0
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
inst✝ : p.IsPrime
hp : p ≠ ⊥
P : Ideal S
hP : P ∈ primesOver S p
⊢ Ideal.map (algebraMap R S) p ≠ ⊥
Tactic:
exact (Ideal.map_eq_bot_iff_of_injective
  (NoZeroSMulDivisors.algebraMap_injective R S)).not.mpr hp
Proof state after:
no goals
Theorem: isUnramifiedAt_iff_normalizedFactors_nodup
Proof state before:
case hP
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
inst✝ : p.IsPrime
hp : p ≠ ⊥
P : Ideal S
hP : P ∈ primesOver S p
⊢ P.IsPrime
Tactic:
exact hP.1
Proof state after:
no goals
Theorem: isUnramifiedAt_iff_normalizedFactors_nodup
Proof state before:
case hP0
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
inst✝ : p.IsPrime
hp : p ≠ ⊥
P : Ideal S
hP : P ∈ primesOver S p
⊢ P ≠ ⊥
Tactic:
exact ne_bot_of_mem_primesOver hp hP
Proof state after:
no goals