Theorem: comap_map_eq_of_isUnramified
Proof state before:
case neg
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 ≠ ⊥
⊢ ∏ i ∈ Finset.filter (fun i => Ideal.comap (algebraMap R S) i = p) (factors I).toFinset,
      i ^ Multiset.count i (factors I) =
    Ideal.map (algebraMap R S) p ^
      if h : p.IsPrime ∧ Ideal.comap (algebraMap R S) I ≤ p then Multiset.count (𝔓 p h) (factors I) else 0

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:
have hpbot' : p.map (algebraMap R S) ≠ ⊥ := (Ideal.map_eq_bot_iff_of_injective hRS).not.mpr hpbot
Proof state after:
case neg
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 ≠ ⊥
⊢ ∏ i ∈ Finset.filter (fun i => Ideal.comap (algebraMap R S) i = p) (factors I).toFinset,
      i ^ Multiset.count i (factors I) =
    Ideal.map (algebraMap R S) p ^
      if h : p.IsPrime ∧ Ideal.comap (algebraMap R S) I ≤ p then Multiset.count (𝔓 p h) (factors I) else 0

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