internlm/Lean-Github huggingface dataset:
Theorem: comap_map_eq_of_isUnramified
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✝¹ : 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)
⊢ Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) I) = I
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✝¹ : 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
⊢ Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) I) = I
Theorem: comap_map_eq_of_isUnramified
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✝¹ : 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
⊢ Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) I) = I
Tactic:
by_cases hIbot : I = ⊥
Proof state after:
case pos
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 = ⊥
⊢ Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) I) = I

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 = ⊥
⊢ Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) I) = I
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 = ⊥
⊢ Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) I) = I
Tactic:
have h1 : Algebra.IsIntegral R S := IsIntegralClosure.isIntegral_algebra R L
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
⊢ Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) I) = I
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
⊢ Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) I) = I
Tactic:
have hIbot' : I.comap (algebraMap R S) ≠ ⊥ := mt Ideal.eq_bot_of_comap_eq_bot hIbot
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 ≠ ⊥
⊢ Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) I) = I
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 ≠ ⊥
⊢ Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) I) = I
Tactic:
have : ∀ p, (p.IsPrime ∧ I.comap (algebraMap R S) ≤ p) → ∃ P ≥ I, P ∈ primesOver S p := by
  intro p ⟨hp₁, hp₂⟩
  exact Ideal.exists_ideal_over_prime_of_isIntegral _ _ hp₂
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 ≠ ⊥
this : ∀ (p : Ideal R), p.IsPrime ∧ Ideal.comap (algebraMap R S) I ≤ p → ∃ P ≥ I, P ∈ primesOver S p
⊢ Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) I) = I
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 ≠ ⊥
this : ∀ (p : Ideal R), p.IsPrime ∧ Ideal.comap (algebraMap R S) I ≤ p → ∃ P ≥ I, P ∈ primesOver S p
⊢ Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) I) = I
Tactic:
choose 𝔓 h𝔓 h𝔓' using this
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
⊢ Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) I) = I
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
⊢ Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) I) = I
Tactic:
suffices I = ∏ p in (factors (I.comap <| algebraMap R S)).toFinset,
  (p.map (algebraMap R S)) ^ (if h : _ then (factors I).count (𝔓 p h) else 0) by
  simp_rw [← Ideal.mapHom_apply, ← map_pow, ← map_prod, Ideal.mapHom_apply] at this
  rw [this, Ideal.map_comap_map]
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
⊢ I =
    ∏ p ∈ (factors (Ideal.comap (algebraMap R S) I)).toFinset,
      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
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
⊢ I =
    ∏ p ∈ (factors (Ideal.comap (algebraMap R S) I)).toFinset,
      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
Tactic:
conv_lhs => rw [← associated_iff_eq.mp (factors_pow_count_prod hIbot)]
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 ∈ (factors I).toFinset, p ^ Multiset.count p (factors I) =
    ∏ p ∈ (factors (Ideal.comap (algebraMap R S) I)).toFinset,
      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
Theorem: comap_map_eq_of_isUnramified
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✝¹ : 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
⊢ Function.Injective ⇑(algebraMap R S)
Tactic:
refine Function.Injective.of_comp (f := algebraMap S 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✝¹ : 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
⊢ Function.Injective (⇑(algebraMap S L) ∘ ⇑(algebraMap R S))
Theorem: comap_map_eq_of_isUnramified
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✝¹ : 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
⊢ Function.Injective (⇑(algebraMap S L) ∘ ⇑(algebraMap R S))
Tactic:
rw [← RingHom.coe_comp, ← IsScalarTower.algebraMap_eq, IsScalarTower.algebraMap_eq R K 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✝¹ : 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
⊢ Function.Injective ⇑((algebraMap K L).comp (algebraMap R K))
Theorem: comap_map_eq_of_isUnramified
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✝¹ : 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
⊢ Function.Injective ⇑((algebraMap K L).comp (algebraMap R K))
Tactic:
exact (algebraMap K L).injective.comp (IsFractionRing.injective _ _)
Proof state after:
no goals
Theorem: comap_map_eq_of_isUnramified
Proof state before:
case pos
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 = ⊥
⊢ Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) I) = I
Tactic:
rw [hIbot, Ideal.comap_bot_of_injective _ hRS, Ideal.map_bot]
Proof state after:
no goals
Theorem: comap_map_eq_of_isUnramified
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✝¹ : 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 → ∃ P ≥ I, P ∈ primesOver S p
Tactic:
intro p ⟨hp₁, 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✝¹ : 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
hp₁ : p.IsPrime
hp₂ : Ideal.comap (algebraMap R S) I ≤ p
⊢ ∃ P ≥ I, P ∈ primesOver S p
Theorem: comap_map_eq_of_isUnramified
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✝¹ : 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
hp₁ : p.IsPrime
hp₂ : Ideal.comap (algebraMap R S) I ≤ p
⊢ ∃ P ≥ I, P ∈ primesOver S p
Tactic:
exact Ideal.exists_ideal_over_prime_of_isIntegral _ _ hp₂
Proof state after:
no goals