Theorem: primesOver_bot (FltRegular/NumberTheory/GaloisPrime.lean)

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
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 ∈ {⊥}

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]
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 = ⊥

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, ?_⟩
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 = ⊥

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
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) ⊥ = ⊥

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]
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)

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 _ _⟩
State after:
no goals