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)
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
this :
  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
⊢ Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) I) = I
Tactic:
simp_rw [← Ideal.mapHom_apply, ← map_pow, ← map_prod, Ideal.mapHom_apply] at this
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) → 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
this :
  I =
    Ideal.map (algebraMap R S)
      (∏ x ∈ (factors (Ideal.comap (algebraMap R S) I)).toFinset,
        x ^ if h : x.IsPrime ∧ Ideal.comap (algebraMap R S) I ≤ x then Multiset.count (𝔓 x h) (factors I) else 0)
⊢ 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
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
this :
  I =
    Ideal.map (algebraMap R S)
      (∏ x ∈ (factors (Ideal.comap (algebraMap R S) I)).toFinset,
        x ^ if h : x.IsPrime ∧ Ideal.comap (algebraMap R S) I ≤ x then Multiset.count (𝔓 x h) (factors I) else 0)
⊢ Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) I) = I
Tactic:
rw [this, Ideal.map_comap_map]
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
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
⊢ Finset.filter (fun i => Ideal.comap (algebraMap R S) i = p) (factors I).toFinset = primesOverFinset S p
Tactic:
ext P
Proof state after:
case neg.h.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
⊢ P ∈ Finset.filter (fun i => Ideal.comap (algebraMap R S) i = p) (factors I).toFinset ↔ P ∈ primesOverFinset S p
Theorem: comap_map_eq_of_isUnramified
Proof state before:
case neg.h.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
⊢ P ∈ Finset.filter (fun i => Ideal.comap (algebraMap R S) i = p) (factors I).toFinset ↔ P ∈ primesOverFinset S p
Tactic:
simp only [factors_eq_normalizedFactors, Multiset.mem_toFinset,
  Ideal.mem_normalizedFactors_iff hpbot', Finset.filter_congr_decidable,
  Ideal.mem_normalizedFactors_iff hIbot, and_imp, Finset.mem_filter]
Proof state after:
case neg.h.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
⊢ (P.IsPrime ∧ I ≤ P) ∧ Ideal.comap (algebraMap R S) P = p ↔ P ∈ primesOverFinset S p
Theorem: comap_map_eq_of_isUnramified
Proof state before:
case neg.h.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
⊢ (P.IsPrime ∧ I ≤ P) ∧ Ideal.comap (algebraMap R S) P = p ↔ P ∈ primesOverFinset S p
Tactic:
rw [← Finset.mem_coe, coe_primesOverFinset S p hpbot]
Proof state after:
case neg.h.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
⊢ (P.IsPrime ∧ I ≤ P) ∧ Ideal.comap (algebraMap R S) P = p ↔ P ∈ primesOver S p
Theorem: comap_map_eq_of_isUnramified
Proof state before:
case neg.h.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
⊢ (P.IsPrime ∧ I ≤ P) ∧ Ideal.comap (algebraMap R S) P = p ↔ P ∈ primesOver S p
Tactic:
refine ⟨fun H ↦ ⟨H.1.1, H.2⟩, fun H ↦ ⟨⟨H.1, ?_⟩, H.2⟩⟩
Proof state after:
case neg.h.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
H : P ∈ primesOver S p
⊢ I ≤ P
Theorem: comap_map_eq_of_isUnramified
Proof state before:
case neg.h.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
H : P ∈ primesOver S p
⊢ I ≤ P
Tactic:
have ⟨σ, hσ⟩ := exists_comap_galRestrict_eq R K L S (h𝔓' _ hp) H
Proof state after:
case neg.h.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
H : P ∈ primesOver S p
σ : L ≃ₐ[K] L
hσ : Ideal.comap ((galRestrict R K L S) σ) (𝔓 p hp) = P
⊢ I ≤ P
Theorem: comap_map_eq_of_isUnramified
Proof state before:
case neg.h.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
H : P ∈ primesOver S p
σ : L ≃ₐ[K] L
hσ : Ideal.comap ((galRestrict R K L S) σ) (𝔓 p hp) = P
⊢ I ≤ P
Tactic:
rw [← hσ, ← hI σ]
Proof state after:
case neg.h.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
H : P ∈ primesOver S p
σ : L ≃ₐ[K] L
hσ : Ideal.comap ((galRestrict R K L S) σ) (𝔓 p hp) = P
⊢ Ideal.comap ((galRestrict R K L S) σ) I ≤ Ideal.comap ((galRestrict R K L S) σ) (𝔓 p hp)
Theorem: comap_map_eq_of_isUnramified
Proof state before:
case neg.h.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
H : P ∈ primesOver S p
σ : L ≃ₐ[K] L
hσ : Ideal.comap ((galRestrict R K L S) σ) (𝔓 p hp) = P
⊢ Ideal.comap ((galRestrict R K L S) σ) I ≤ Ideal.comap ((galRestrict R K L S) σ) (𝔓 p hp)
Tactic:
exact Ideal.comap_mono (h𝔓 _ hp)
Proof state after:
no goals