internlm/Lean-Github huggingface dataset:
Theorem: unit_inv_conj_is_root_of_unity
Proof state before:
case refine_3.intro.intro.inr
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
h : p ≠ 2
hp : (↑p).Prime
u : (𝓞 K)ˣ
hpo : Odd ↑p
this✝ : NormedAlgebra ℚ ℂ
this : ∃ n, ∃ (_ : 0 < n), ((algebraMap (𝓞 K) K) ↑u * (algebraMap (𝓞 K) K) ↑((unitGalConj K p) u)⁻¹) ^ n = 1
n : ℕ
k : ℕ+
hk : Odd ↑k
x✝ : ¬∃ m, u * ((unitGalConj K p) u)⁻¹ = hζ.unit' ^ (m * 2)
hz : (algebraMap (𝓞 K) K) ↑u * (algebraMap (𝓞 K) K) ↑((unitGalConj K p) u)⁻¹ = -(algebraMap (𝓞 K) K) ↑hζ.unit' ^ n
⊢ False
Tactic:
rw [← map_mul, ← Units.val_mul, ← map_pow, ←  Units.val_pow_eq_pow_val, ← map_neg] at hz
Proof state after:
case refine_3.intro.intro.inr
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
h : p ≠ 2
hp : (↑p).Prime
u : (𝓞 K)ˣ
hpo : Odd ↑p
this✝ : NormedAlgebra ℚ ℂ
this : ∃ n, ∃ (_ : 0 < n), ((algebraMap (𝓞 K) K) ↑u * (algebraMap (𝓞 K) K) ↑((unitGalConj K p) u)⁻¹) ^ n = 1
n : ℕ
k : ℕ+
hk : Odd ↑k
x✝ : ¬∃ m, u * ((unitGalConj K p) u)⁻¹ = hζ.unit' ^ (m * 2)
hz : (algebraMap (𝓞 K) K) ↑(u * ((unitGalConj K p) u)⁻¹) = (algebraMap (𝓞 K) K) (-↑(hζ.unit' ^ n))
⊢ False
Theorem: unit_inv_conj_is_root_of_unity
Proof state before:
case refine_3.intro.intro.inr
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
h : p ≠ 2
hp : (↑p).Prime
u : (𝓞 K)ˣ
hpo : Odd ↑p
this✝ : NormedAlgebra ℚ ℂ
this : ∃ n, ∃ (_ : 0 < n), ((algebraMap (𝓞 K) K) ↑u * (algebraMap (𝓞 K) K) ↑((unitGalConj K p) u)⁻¹) ^ n = 1
n : ℕ
k : ℕ+
hk : Odd ↑k
x✝ : ¬∃ m, u * ((unitGalConj K p) u)⁻¹ = hζ.unit' ^ (m * 2)
hz : (algebraMap (𝓞 K) K) ↑(u * ((unitGalConj K p) u)⁻¹) = (algebraMap (𝓞 K) K) (-↑(hζ.unit' ^ n))
⊢ False
Tactic:
norm_cast at hz
Proof state after:
case refine_3.intro.intro.inr
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
h : p ≠ 2
hp : (↑p).Prime
u : (𝓞 K)ˣ
hpo : Odd ↑p
this✝ : NormedAlgebra ℚ ℂ
this : ∃ n, ∃ (_ : 0 < n), ((algebraMap (𝓞 K) K) ↑u * (algebraMap (𝓞 K) K) ↑((unitGalConj K p) u)⁻¹) ^ n = 1
n : ℕ
k : ℕ+
hk : Odd ↑k
x✝ : ¬∃ m, u * ((unitGalConj K p) u)⁻¹ = hζ.unit' ^ (m * 2)
hz : u * ((unitGalConj K p) u)⁻¹ = -hζ.unit' ^ n
⊢ False
Theorem: unit_inv_conj_is_root_of_unity
Proof state before:
case refine_3.intro.intro.inr
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
h : p ≠ 2
hp : (↑p).Prime
u : (𝓞 K)ˣ
hpo : Odd ↑p
this✝ : NormedAlgebra ℚ ℂ
this : ∃ n, ∃ (_ : 0 < n), ((algebraMap (𝓞 K) K) ↑u * (algebraMap (𝓞 K) K) ↑((unitGalConj K p) u)⁻¹) ^ n = 1
n : ℕ
k : ℕ+
hk : Odd ↑k
x✝ : ¬∃ m, u * ((unitGalConj K p) u)⁻¹ = hζ.unit' ^ (m * 2)
hz : u * ((unitGalConj K p) u)⁻¹ = -hζ.unit' ^ n
⊢ False
Tactic:
simpa [hz] using unit_inv_conj_not_neg_zeta_runity hζ h u n hp
Proof state after:
no goals
Theorem: unit_inv_conj_is_root_of_unity
Proof state before:
case refine_1
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
h : p ≠ 2
hp : (↑p).Prime
u : (𝓞 K)ˣ
hpo : Odd ↑p
this : NormedAlgebra ℚ ℂ
⊢ IsIntegral ℤ ((algebraMap (𝓞 K) K) ↑u * (algebraMap (𝓞 K) K) ↑((unitGalConj K p) u)⁻¹)
Tactic:
apply RingHom.IsIntegralElem.mul
Proof state after:
case refine_1.hx
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
h : p ≠ 2
hp : (↑p).Prime
u : (𝓞 K)ˣ
hpo : Odd ↑p
this : NormedAlgebra ℚ ℂ
⊢ (algebraMap ℤ K).IsIntegralElem ((algebraMap (𝓞 K) K) ↑u)

case refine_1.hy
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
h : p ≠ 2
hp : (↑p).Prime
u : (𝓞 K)ˣ
hpo : Odd ↑p
this : NormedAlgebra ℚ ℂ
⊢ (algebraMap ℤ K).IsIntegralElem ((algebraMap (𝓞 K) K) ↑((unitGalConj K p) u)⁻¹)
Theorem: unit_inv_conj_is_root_of_unity
Proof state before:
case refine_1.hx
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
h : p ≠ 2
hp : (↑p).Prime
u : (𝓞 K)ˣ
hpo : Odd ↑p
this : NormedAlgebra ℚ ℂ
⊢ (algebraMap ℤ K).IsIntegralElem ((algebraMap (𝓞 K) K) ↑u)
Tactic:
exact NumberField.RingOfIntegers.isIntegral_coe _
Proof state after:
no goals
Theorem: unit_inv_conj_is_root_of_unity
Proof state before:
case refine_1.hy
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
h : p ≠ 2
hp : (↑p).Prime
u : (𝓞 K)ˣ
hpo : Odd ↑p
this : NormedAlgebra ℚ ℂ
⊢ (algebraMap ℤ K).IsIntegralElem ((algebraMap (𝓞 K) K) ↑((unitGalConj K p) u)⁻¹)
Tactic:
exact NumberField.RingOfIntegers.isIntegral_coe _
Proof state after:
no goals
Theorem: unit_inv_conj_is_root_of_unity
Proof state before:
case refine_2
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
h : p ≠ 2
hp : (↑p).Prime
u : (𝓞 K)ˣ
hpo : Odd ↑p
this : NormedAlgebra ℚ ℂ
⊢ ∀ (φ : K →+* ℂ), ‖φ ((algebraMap (𝓞 K) K) ↑u * (algebraMap (𝓞 K) K) ↑((unitGalConj K p) u)⁻¹)‖ = 1
Tactic:
exact unit_lemma_val_one p u
Proof state after:
no goals
Theorem: inv_coe_coe
Proof state before:
p : ℕ+
K✝ : Type ?u.244158
inst✝⁵ : Field K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p
inst✝⁴ : NumberField K✝
inst✝³ : IsCyclotomicExtension {p} ℚ K✝
K : Type u_1
A : Type u_2
inst✝² : Field K
inst✝¹ : SetLike A K
inst✝ : SubsemiringClass A K
S : A
s : (↥S)ˣ
⊢ (↑↑s)⁻¹ = ↑↑s⁻¹
Tactic:
apply inv_eq_of_mul_eq_one_right
Proof state after:
case a
p : ℕ+
K✝ : Type ?u.244158
inst✝⁵ : Field K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p
inst✝⁴ : NumberField K✝
inst✝³ : IsCyclotomicExtension {p} ℚ K✝
K : Type u_1
A : Type u_2
inst✝² : Field K
inst✝¹ : SetLike A K
inst✝ : SubsemiringClass A K
S : A
s : (↥S)ˣ
⊢ ↑↑s * ↑↑s⁻¹ = 1
Theorem: inv_coe_coe
Proof state before:
case a
p : ℕ+
K✝ : Type ?u.244158
inst✝⁵ : Field K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p
inst✝⁴ : NumberField K✝
inst✝³ : IsCyclotomicExtension {p} ℚ K✝
K : Type u_1
A : Type u_2
inst✝² : Field K
inst✝¹ : SetLike A K
inst✝ : SubsemiringClass A K
S : A
s : (↥S)ˣ
⊢ ↑↑s * ↑↑s⁻¹ = 1
Tactic:
change ((s * s⁻¹ : Sˣ) : K) = 1
Proof state after:
case a
p : ℕ+
K✝ : Type ?u.244158
inst✝⁵ : Field K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p
inst✝⁴ : NumberField K✝
inst✝³ : IsCyclotomicExtension {p} ℚ K✝
K : Type u_1
A : Type u_2
inst✝² : Field K
inst✝¹ : SetLike A K
inst✝ : SubsemiringClass A K
S : A
s : (↥S)ˣ
⊢ ↑↑(s * s⁻¹) = 1
Theorem: inv_coe_coe
Proof state before:
case a
p : ℕ+
K✝ : Type ?u.244158
inst✝⁵ : Field K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p
inst✝⁴ : NumberField K✝
inst✝³ : IsCyclotomicExtension {p} ℚ K✝
K : Type u_1
A : Type u_2
inst✝² : Field K
inst✝¹ : SetLike A K
inst✝ : SubsemiringClass A K
S : A
s : (↥S)ˣ
⊢ ↑↑(s * s⁻¹) = 1
Tactic:
rw [mul_inv_self]
Proof state after:
case a
p : ℕ+
K✝ : Type ?u.244158
inst✝⁵ : Field K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p
inst✝⁴ : NumberField K✝
inst✝³ : IsCyclotomicExtension {p} ℚ K✝
K : Type u_1
A : Type u_2
inst✝² : Field K
inst✝¹ : SetLike A K
inst✝ : SubsemiringClass A K
S : A
s : (↥S)ˣ
⊢ ↑↑1 = 1
Theorem: inv_coe_coe
Proof state before:
case a
p : ℕ+
K✝ : Type ?u.244158
inst✝⁵ : Field K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p
inst✝⁴ : NumberField K✝
inst✝³ : IsCyclotomicExtension {p} ℚ K✝
K : Type u_1
A : Type u_2
inst✝² : Field K
inst✝¹ : SetLike A K
inst✝ : SubsemiringClass A K
S : A
s : (↥S)ˣ
⊢ ↑↑1 = 1
Tactic:
rfl
Proof state after:
no goals
Theorem: IsPrimitiveRoot.eq_one_mod_one_sub'
Proof state before:
p : ℕ+
K : Type ?u.247041
inst✝⁴ : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝³ : NumberField K
inst✝² : IsCyclotomicExtension {p} ℚ K
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsDomain A
n : ℕ+
ζ : A
hζ : IsPrimitiveRoot ζ ↑n
η : A
hη : η ∈ nthRootsFinset (↑n) A
⊢ (Ideal.Quotient.mk (Ideal.span {ζ - 1})) η = 1
Tactic:
obtain ⟨i, ⟨_, rfl⟩⟩ := hζ.eq_pow_of_pow_eq_one ((Polynomial.mem_nthRootsFinset n.2).1 hη) n.2
Proof state after:
case intro.intro
p : ℕ+
K : Type ?u.247041
inst✝⁴ : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝³ : NumberField K
inst✝² : IsCyclotomicExtension {p} ℚ K
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsDomain A
n : ℕ+
ζ : A
hζ : IsPrimitiveRoot ζ ↑n
i : ℕ
left✝ : i < ↑n
hη : ζ ^ i ∈ nthRootsFinset (↑n) A
⊢ (Ideal.Quotient.mk (Ideal.span {ζ - 1})) (ζ ^ i) = 1
Theorem: IsPrimitiveRoot.eq_one_mod_one_sub'
Proof state before:
case intro.intro
p : ℕ+
K : Type ?u.247041
inst✝⁴ : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝³ : NumberField K
inst✝² : IsCyclotomicExtension {p} ℚ K
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsDomain A
n : ℕ+
ζ : A
hζ : IsPrimitiveRoot ζ ↑n
i : ℕ
left✝ : i < ↑n
hη : ζ ^ i ∈ nthRootsFinset (↑n) A
⊢ (Ideal.Quotient.mk (Ideal.span {ζ - 1})) (ζ ^ i) = 1
Tactic:
rw [map_pow, ← Ideal.Quotient.algebraMap_eq, eq_one_mod_one_sub, one_pow]
Proof state after:
no goals
Theorem: primesOver_bot
Proof state before:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : Nontrivial R
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : Algebra.IsIntegral R S
⊢ primesOver S ⊥ = {⊥}
Tactic:
ext p
Proof state after:
case h
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : Nontrivial R
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : Algebra.IsIntegral R S
p : Ideal S
⊢ p ∈ primesOver S ⊥ ↔ p ∈ {⊥}
Theorem: primesOver_bot
Proof state before:
case h
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : Nontrivial R
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : Algebra.IsIntegral R S
p : Ideal S
⊢ p ∈ primesOver S ⊥ ↔ p ∈ {⊥}
Tactic:
simp only [primesOver, Set.mem_setOf_eq, Set.mem_singleton_iff]
Proof state after:
case h
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : Nontrivial R
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : Algebra.IsIntegral R S
p : Ideal S
⊢ p.IsPrime ∧ Ideal.comap (algebraMap R S) p = ⊥ ↔ p = ⊥
Theorem: primesOver_bot
Proof state before:
case h
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : Nontrivial R
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : Algebra.IsIntegral R S
p : Ideal S
⊢ p.IsPrime ∧ Ideal.comap (algebraMap R S) p = ⊥ ↔ p = ⊥
Tactic:
refine ⟨fun H ↦ Ideal.eq_bot_of_comap_eq_bot H.2, ?_⟩
Proof state after:
case h
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : Nontrivial R
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : Algebra.IsIntegral R S
p : Ideal S
⊢ p = ⊥ → p.IsPrime ∧ Ideal.comap (algebraMap R S) p = ⊥
Theorem: primesOver_bot
Proof state before:
case h
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : Nontrivial R
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : Algebra.IsIntegral R S
p : Ideal S
⊢ p = ⊥ → p.IsPrime ∧ Ideal.comap (algebraMap R S) p = ⊥
Tactic:
rintro rfl
Proof state after:
case h
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : Nontrivial R
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : Algebra.IsIntegral R S
⊢ ⊥.IsPrime ∧ Ideal.comap (algebraMap R S) ⊥ = ⊥
Theorem: primesOver_bot
Proof state before:
case h
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : Nontrivial R
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : Algebra.IsIntegral R S
⊢ ⊥.IsPrime ∧ Ideal.comap (algebraMap R S) ⊥ = ⊥
Tactic:
rw [← RingHom.ker_eq_comap_bot, ← RingHom.injective_iff_ker_eq_bot]
Proof state after:
case h
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : Nontrivial R
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : Algebra.IsIntegral R S
⊢ ⊥.IsPrime ∧ Function.Injective ⇑(algebraMap R S)
Theorem: primesOver_bot
Proof state before:
case h
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : Nontrivial R
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : Algebra.IsIntegral R S
⊢ ⊥.IsPrime ∧ Function.Injective ⇑(algebraMap R S)
Tactic:
exact ⟨Ideal.bot_prime, NoZeroSMulDivisors.algebraMap_injective _ _⟩
Proof state after:
no goals
Theorem: primesOverFinset_bot
Proof state before:
R : Type u_2
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsDedekindDomain S
⊢ primesOverFinset S ⊥ = ∅
Tactic:
classical
rw [primesOverFinset, Ideal.map_bot, ← Ideal.zero_eq_bot, factors_zero]
rfl
Proof state after:
no goals
Theorem: primesOverFinset_bot
Proof state before:
R : Type u_2
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsDedekindDomain S
⊢ primesOverFinset S ⊥ = ∅
Tactic:
rw [primesOverFinset, Ideal.map_bot, ← Ideal.zero_eq_bot, factors_zero]
Proof state after:
R : Type u_2
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsDedekindDomain S
⊢ Multiset.toFinset 0 = ∅
Theorem: primesOverFinset_bot
Proof state before:
R : Type u_2
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsDedekindDomain S
⊢ Multiset.toFinset 0 = ∅
Tactic:
rfl
Proof state after:
no goals
Theorem: coe_primesOverFinset
Proof state before:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Ring.DimensionLEOne R
inst✝¹ : IsDedekindDomain S
inst✝ : NoZeroSMulDivisors R S
p : Ideal R
hp : p ≠ ⊥
hp' : p.IsPrime
⊢ ↑(primesOverFinset S p) = primesOver S p
Tactic:
classical
ext P
have : p.map (algebraMap R S) ≠ ⊥ := by
  rwa [Ne, Ideal.map_eq_bot_iff_of_injective (NoZeroSMulDivisors.algebraMap_injective R S)]
simp only [Finset.mem_coe, Multiset.mem_toFinset, Ideal.mem_normalizedFactors_iff this,
  factors_eq_normalizedFactors, Ideal.map_le_iff_le_comap, primesOverFinset]
exact ⟨fun H ↦ ⟨H.1, ((hp'.isMaximal hp).eq_of_le (H.1.comap _).ne_top H.2).symm⟩,
  fun H ↦ ⟨H.1, H.2.ge⟩⟩
Proof state after:
no goals
Theorem: coe_primesOverFinset
Proof state before:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Ring.DimensionLEOne R
inst✝¹ : IsDedekindDomain S
inst✝ : NoZeroSMulDivisors R S
p : Ideal R
hp : p ≠ ⊥
hp' : p.IsPrime
⊢ ↑(primesOverFinset S p) = primesOver S p
Tactic:
ext P
Proof state after:
case h
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Ring.DimensionLEOne R
inst✝¹ : IsDedekindDomain S
inst✝ : NoZeroSMulDivisors R S
p : Ideal R
hp : p ≠ ⊥
hp' : p.IsPrime
P : Ideal S
⊢ P ∈ ↑(primesOverFinset S p) ↔ P ∈ primesOver S p
Theorem: coe_primesOverFinset
Proof state before:
case h
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Ring.DimensionLEOne R
inst✝¹ : IsDedekindDomain S
inst✝ : NoZeroSMulDivisors R S
p : Ideal R
hp : p ≠ ⊥
hp' : p.IsPrime
P : Ideal S
⊢ P ∈ ↑(primesOverFinset S p) ↔ P ∈ primesOver S p
Tactic:
have : p.map (algebraMap R S) ≠ ⊥ := by
  rwa [Ne, Ideal.map_eq_bot_iff_of_injective (NoZeroSMulDivisors.algebraMap_injective R S)]
Proof state after:
case h
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Ring.DimensionLEOne R
inst✝¹ : IsDedekindDomain S
inst✝ : NoZeroSMulDivisors R S
p : Ideal R
hp : p ≠ ⊥
hp' : p.IsPrime
P : Ideal S
this : Ideal.map (algebraMap R S) p ≠ ⊥
⊢ P ∈ ↑(primesOverFinset S p) ↔ P ∈ primesOver S p
Theorem: coe_primesOverFinset
Proof state before:
case h
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Ring.DimensionLEOne R
inst✝¹ : IsDedekindDomain S
inst✝ : NoZeroSMulDivisors R S
p : Ideal R
hp : p ≠ ⊥
hp' : p.IsPrime
P : Ideal S
this : Ideal.map (algebraMap R S) p ≠ ⊥
⊢ P ∈ ↑(primesOverFinset S p) ↔ P ∈ primesOver S p
Tactic:
simp only [Finset.mem_coe, Multiset.mem_toFinset, Ideal.mem_normalizedFactors_iff this,
  factors_eq_normalizedFactors, Ideal.map_le_iff_le_comap, primesOverFinset]
Proof state after:
case h
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Ring.DimensionLEOne R
inst✝¹ : IsDedekindDomain S
inst✝ : NoZeroSMulDivisors R S
p : Ideal R
hp : p ≠ ⊥
hp' : p.IsPrime
P : Ideal S
this : Ideal.map (algebraMap R S) p ≠ ⊥
⊢ P.IsPrime ∧ p ≤ Ideal.comap (algebraMap R S) P ↔ P ∈ primesOver S p
Theorem: coe_primesOverFinset
Proof state before:
case h
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Ring.DimensionLEOne R
inst✝¹ : IsDedekindDomain S
inst✝ : NoZeroSMulDivisors R S
p : Ideal R
hp : p ≠ ⊥
hp' : p.IsPrime
P : Ideal S
this : Ideal.map (algebraMap R S) p ≠ ⊥
⊢ P.IsPrime ∧ p ≤ Ideal.comap (algebraMap R S) P ↔ P ∈ primesOver S p
Tactic:
exact ⟨fun H ↦ ⟨H.1, ((hp'.isMaximal hp).eq_of_le (H.1.comap _).ne_top H.2).symm⟩,
  fun H ↦ ⟨H.1, H.2.ge⟩⟩
Proof state after:
no goals
Theorem: coe_primesOverFinset
Proof state before:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Ring.DimensionLEOne R
inst✝¹ : IsDedekindDomain S
inst✝ : NoZeroSMulDivisors R S
p : Ideal R
hp : p ≠ ⊥
hp' : p.IsPrime
P : Ideal S
⊢ Ideal.map (algebraMap R S) p ≠ ⊥
Tactic:
rwa [Ne, Ideal.map_eq_bot_iff_of_injective (NoZeroSMulDivisors.algebraMap_injective R S)]
Proof state after:
no goals
Theorem: primesOver_eq_empty_of_not_isPrime
Proof state before:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : Ideal R
hp : ¬p.IsPrime
⊢ primesOver S p = ∅
Tactic:
rw [← Set.not_nonempty_iff_eq_empty]
Proof state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : Ideal R
hp : ¬p.IsPrime
⊢ ¬(primesOver S p).Nonempty
Theorem: primesOver_eq_empty_of_not_isPrime
Proof state before:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : Ideal R
hp : ¬p.IsPrime
⊢ ¬(primesOver S p).Nonempty
Tactic:
rintro ⟨P, hP⟩
Proof state after:
case intro
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : Ideal R
hp : ¬p.IsPrime
P : Ideal S
hP : P ∈ primesOver S p
⊢ False
Theorem: primesOver_eq_empty_of_not_isPrime
Proof state before:
case intro
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : Ideal R
hp : ¬p.IsPrime
P : Ideal S
hP : P ∈ primesOver S p
⊢ False
Tactic:
exact hp (hP.2 ▸ hP.1.comap _)
Proof state after:
no goals
Theorem: primesOver_finite
Proof state before:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Ring.DimensionLEOne R
inst✝¹ : IsDedekindDomain S
inst✝ : NoZeroSMulDivisors R S
p : Ideal R
hp : p ≠ ⊥
⊢ (primesOver S p).Finite
Tactic:
by_cases h: p.IsPrime
Proof state after:
case pos
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Ring.DimensionLEOne R
inst✝¹ : IsDedekindDomain S
inst✝ : NoZeroSMulDivisors R S
p : Ideal R
hp : p ≠ ⊥
h : p.IsPrime
⊢ (primesOver S p).Finite

case neg
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Ring.DimensionLEOne R
inst✝¹ : IsDedekindDomain S
inst✝ : NoZeroSMulDivisors R S
p : Ideal R
hp : p ≠ ⊥
h : ¬p.IsPrime
⊢ (primesOver S p).Finite
Theorem: primesOver_finite
Proof state before:
case pos
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Ring.DimensionLEOne R
inst✝¹ : IsDedekindDomain S
inst✝ : NoZeroSMulDivisors R S
p : Ideal R
hp : p ≠ ⊥
h : p.IsPrime
⊢ (primesOver S p).Finite
Tactic:
classical
rw [← coe_primesOverFinset S p hp]
exact Finset.finite_toSet _
Proof state after:
no goals
Theorem: primesOver_finite
Proof state before:
case pos
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Ring.DimensionLEOne R
inst✝¹ : IsDedekindDomain S
inst✝ : NoZeroSMulDivisors R S
p : Ideal R
hp : p ≠ ⊥
h : p.IsPrime
⊢ (primesOver S p).Finite
Tactic:
rw [← coe_primesOverFinset S p hp]
Proof state after:
case pos
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Ring.DimensionLEOne R
inst✝¹ : IsDedekindDomain S
inst✝ : NoZeroSMulDivisors R S
p : Ideal R
hp : p ≠ ⊥
h : p.IsPrime
⊢ (↑(primesOverFinset S p)).Finite
Theorem: primesOver_finite
Proof state before:
case pos
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Ring.DimensionLEOne R
inst✝¹ : IsDedekindDomain S
inst✝ : NoZeroSMulDivisors R S
p : Ideal R
hp : p ≠ ⊥
h : p.IsPrime
⊢ (↑(primesOverFinset S p)).Finite
Tactic:
exact Finset.finite_toSet _
Proof state after:
no goals
Theorem: primesOver_finite
Proof state before:
case neg
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Ring.DimensionLEOne R
inst✝¹ : IsDedekindDomain S
inst✝ : NoZeroSMulDivisors R S
p : Ideal R
hp : p ≠ ⊥
h : ¬p.IsPrime
⊢ (primesOver S p).Finite
Tactic:
rw [primesOver_eq_empty_of_not_isPrime S p h]
Proof state after:
case neg
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Ring.DimensionLEOne R
inst✝¹ : IsDedekindDomain S
inst✝ : NoZeroSMulDivisors R S
p : Ideal R
hp : p ≠ ⊥
h : ¬p.IsPrime
⊢ ∅.Finite
Theorem: primesOver_finite
Proof state before:
case neg
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Ring.DimensionLEOne R
inst✝¹ : IsDedekindDomain S
inst✝ : NoZeroSMulDivisors R S
p : Ideal R
hp : p ≠ ⊥
h : ¬p.IsPrime
⊢ ∅.Finite
Tactic:
exact Set.finite_empty
Proof state after:
no goals
Theorem: primesOver_nonempty
Proof state before:
R : Type u_2
S : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Algebra.IsIntegral R S
p : Ideal R
inst✝ : p.IsPrime
⊢ (primesOver S p).Nonempty
Tactic:
have := Ideal.bot_prime (α := S)
Proof state after:
R : Type u_2
S : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Algebra.IsIntegral R S
p : Ideal R
inst✝ : p.IsPrime
this : ⊥.IsPrime
⊢ (primesOver S p).Nonempty
Theorem: primesOver_nonempty
Proof state before:
R : Type u_2
S : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Algebra.IsIntegral R S
p : Ideal R
inst✝ : p.IsPrime
this : ⊥.IsPrime
⊢ (primesOver S p).Nonempty
Tactic:
obtain ⟨Q, _, hQ⟩ := Ideal.exists_ideal_over_prime_of_isIntegral p ⊥
  (by rw [Ideal.comap_bot_of_injective _
    (NoZeroSMulDivisors.algebraMap_injective R S)]; exact bot_le)
Proof state after:
case intro.intro
R : Type u_2
S : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Algebra.IsIntegral R S
p : Ideal R
inst✝ : p.IsPrime
this : ⊥.IsPrime
Q : Ideal S
left✝ : Q ≥ ⊥
hQ : Q.IsPrime ∧ Ideal.comap (algebraMap R S) Q = p
⊢ (primesOver S p).Nonempty
Theorem: primesOver_nonempty
Proof state before:
case intro.intro
R : Type u_2
S : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Algebra.IsIntegral R S
p : Ideal R
inst✝ : p.IsPrime
this : ⊥.IsPrime
Q : Ideal S
left✝ : Q ≥ ⊥
hQ : Q.IsPrime ∧ Ideal.comap (algebraMap R S) Q = p
⊢ (primesOver S p).Nonempty
Tactic:
exact ⟨Q, hQ⟩
Proof state after:
no goals
Theorem: primesOver_nonempty
Proof state before:
R : Type u_2
S : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Algebra.IsIntegral R S
p : Ideal R
inst✝ : p.IsPrime
this : ⊥.IsPrime
⊢ Ideal.comap (algebraMap R ?m.22477) ⊥ ≤ p
Tactic:
rw [Ideal.comap_bot_of_injective _
(NoZeroSMulDivisors.algebraMap_injective R S)]
Proof state after:
R : Type u_2
S : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Algebra.IsIntegral R S
p : Ideal R
inst✝ : p.IsPrime
this : ⊥.IsPrime
⊢ ⊥ ≤ p