R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : LocalRing R
x : PrimeSpectrum (ResidueField R)
⊢ ↑(PrimeSpectrum.comap (residue R)) ⊥ = closedPoint R
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : LocalRing R
x : PrimeSpectrum (ResidueField R)
⊢ ↑(PrimeSpectrum.comap (residue R)) x = closedPoint R
rw [Subsingleton.elim x ⊥]
case asIdeal
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : LocalRing R
x : PrimeSpectrum (ResidueField R)
⊢ (↑(PrimeSpectrum.comap (residue R)) ⊥).asIdeal = (closedPoint R).asIdeal
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : LocalRing R
x : PrimeSpectrum (ResidueField R)
⊢ ↑(PrimeSpectrum.comap (residue R)) ⊥ = closedPoint R
ext1
no goals
case asIdeal
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : LocalRing R
x : PrimeSpectrum (ResidueField R)
⊢ (↑(PrimeSpectrum.comap (residue R)) ⊥).asIdeal = (closedPoint R).asIdeal
exact Ideal.mk_ker