internlm/Lean-Github huggingface dataset:
Theorem: comap_map_eq_of_isUnramified
Proof state before:
case neg.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
⊢ ∀ x ∈ primesOverFinset S p,
    x ^ Multiset.count x (factors I) =
      x ^ if h : p.IsPrime ∧ Ideal.comap (algebraMap R S) I ≤ p then Multiset.count (𝔓 p h) (factors I) else 0
Tactic:
intro P hP
Proof state after:
case neg.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 ∈ primesOverFinset S p
⊢ P ^ Multiset.count P (factors I) =
    P ^ if h : p.IsPrime ∧ Ideal.comap (algebraMap R S) I ≤ p then Multiset.count (𝔓 p h) (factors I) else 0
Theorem: comap_map_eq_of_isUnramified
Proof state before:
case neg.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 ∈ primesOverFinset S p
⊢ P ^ Multiset.count P (factors I) =
    P ^ if h : p.IsPrime ∧ Ideal.comap (algebraMap R S) I ≤ p then Multiset.count (𝔓 p h) (factors I) else 0
Tactic:
rw [← Finset.mem_coe, coe_primesOverFinset S p hpbot] at hP
Proof state after:
case neg.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
⊢ P ^ Multiset.count P (factors I) =
    P ^ if h : p.IsPrime ∧ Ideal.comap (algebraMap R S) I ≤ p then Multiset.count (𝔓 p h) (factors I) else 0
Theorem: comap_map_eq_of_isUnramified
Proof state before:
case neg.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
⊢ P ^ Multiset.count P (factors I) =
    P ^ if h : p.IsPrime ∧ Ideal.comap (algebraMap R S) I ≤ p then Multiset.count (𝔓 p h) (factors I) else 0
Tactic:
congr
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
⊢ Multiset.count P (factors I) =
    if h : p.IsPrime ∧ Ideal.comap (algebraMap R S) I ≤ p then Multiset.count (𝔓 p h) (factors I) else 0
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
⊢ Multiset.count P (factors I) =
    if h : p.IsPrime ∧ Ideal.comap (algebraMap R S) I ≤ p then Multiset.count (𝔓 p h) (factors I) else 0
Tactic:
rw [dif_pos hp]
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
⊢ Multiset.count P (factors I) = Multiset.count (𝔓 p hp) (factors I)
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
⊢ Multiset.count P (factors I) = Multiset.count (𝔓 p hp) (factors I)
Tactic:
apply PartENat.natCast_inj.mp
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
⊢ ↑(Multiset.count P (factors I)) = ↑(Multiset.count (𝔓 p hp) (factors I))
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
⊢ ↑(Multiset.count P (factors I)) = ↑(Multiset.count (𝔓 p hp) (factors I))
Tactic:
rw [← normalize_eq P, factors_eq_normalizedFactors,
  ← multiplicity_eq_count_normalizedFactors
    (prime_of_mem_primesOver hpbot hP).irreducible hIbot,
  ← normalize_eq (𝔓 p hp), ← multiplicity_eq_count_normalizedFactors
    (prime_of_mem_primesOver hpbot <| h𝔓' p hp).irreducible hIbot,
  multiplicity.multiplicity_eq_multiplicity_iff]
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 : ℕ), P ^ n ∣ I ↔ 𝔓 p hp ^ n ∣ I
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 : ℕ), P ^ n ∣ I ↔ 𝔓 p hp ^ n ∣ I
Tactic:
intro n
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 : ℕ
⊢ P ^ n ∣ I ↔ 𝔓 p hp ^ n ∣ I
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 : ℕ
⊢ P ^ n ∣ I ↔ 𝔓 p hp ^ n ∣ I
Tactic:
have ⟨σ, hσ⟩ := exists_comap_galRestrict_eq R K L S (h𝔓' _ hp) hP
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
⊢ P ^ n ∣ I ↔ 𝔓 p hp ^ n ∣ I