R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hf : Function.Surjective ↑(Quotient.mk I)
⊢ jacobson I = I ↔ jacobson ⊥ = ⊥
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
⊢ jacobson I = I ↔ jacobson ⊥ = ⊥
have hf : Function.Surjective (Ideal.Quotient.mk I) := Submodule.Quotient.mk_surjective I
case mp
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hf : Function.Surjective ↑(Quotient.mk I)
⊢ jacobson I = I → jacobson ⊥ = ⊥

case mpr
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hf : Function.Surjective ↑(Quotient.mk I)
⊢ jacobson ⊥ = ⊥ → jacobson I = I
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hf : Function.Surjective ↑(Quotient.mk I)
⊢ jacobson I = I ↔ jacobson ⊥ = ⊥
constructor
case mp
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hf : Function.Surjective ↑(Quotient.mk I)
h : jacobson I = I
⊢ jacobson ⊥ = ⊥
case mp
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hf : Function.Surjective ↑(Quotient.mk I)
⊢ jacobson I = I → jacobson ⊥ = ⊥
intro h
case mp
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hf : Function.Surjective ↑(Quotient.mk I)
h : map (Quotient.mk I) (jacobson I) = map (Quotient.mk I) I
⊢ jacobson ⊥ = ⊥
case mp
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hf : Function.Surjective ↑(Quotient.mk I)
h : jacobson I = I
⊢ jacobson ⊥ = ⊥
replace h := congr_arg (Ideal.map (Ideal.Quotient.mk I)) h
case mp
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hf : Function.Surjective ↑(Quotient.mk I)
h : jacobson (map (Quotient.mk I) I) = map (Quotient.mk I) I
⊢ jacobson ⊥ = ⊥
case mp
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hf : Function.Surjective ↑(Quotient.mk I)
h : map (Quotient.mk I) (jacobson I) = map (Quotient.mk I) I
⊢ jacobson ⊥ = ⊥
rw [map_jacobson_of_surjective hf (le_of_eq mk_ker)] at h
no goals
case mp
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hf : Function.Surjective ↑(Quotient.mk I)
h : jacobson (map (Quotient.mk I) I) = map (Quotient.mk I) I
⊢ jacobson ⊥ = ⊥
simpa using h
case mpr
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hf : Function.Surjective ↑(Quotient.mk I)
h : jacobson ⊥ = ⊥
⊢ jacobson I = I
case mpr
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hf : Function.Surjective ↑(Quotient.mk I)
⊢ jacobson ⊥ = ⊥ → jacobson I = I
intro h
case mpr
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hf : Function.Surjective ↑(Quotient.mk I)
h : comap (Quotient.mk I) (jacobson ⊥) = comap (Quotient.mk I) ⊥
⊢ jacobson I = I
case mpr
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hf : Function.Surjective ↑(Quotient.mk I)
h : jacobson ⊥ = ⊥
⊢ jacobson I = I
replace h := congr_arg (comap (Ideal.Quotient.mk I)) h
case mpr
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hf : Function.Surjective ↑(Quotient.mk I)
h : jacobson (RingHom.ker (Quotient.mk I)) = RingHom.ker (Quotient.mk I)
⊢ jacobson I = I
case mpr
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hf : Function.Surjective ↑(Quotient.mk I)
h : comap (Quotient.mk I) (jacobson ⊥) = comap (Quotient.mk I) ⊥
⊢ jacobson I = I
rw [comap_jacobson_of_surjective hf, ← RingHom.ker_eq_comap_bot (Ideal.Quotient.mk I)] at h
no goals
case mpr
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hf : Function.Surjective ↑(Quotient.mk I)
h : jacobson (RingHom.ker (Quotient.mk I)) = RingHom.ker (Quotient.mk I)
⊢ jacobson I = I
simpa using h