case h
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J✝ : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
I : Ideal S
J : Ideal R
⊢ J ∈ Ideal.minimalPrimes (comap f I) ↔ J ∈ comap f '' Ideal.minimalPrimes I
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
I : Ideal S
⊢ Ideal.minimalPrimes (comap f I) = comap f '' Ideal.minimalPrimes I
ext J
case h.mp
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J✝ : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
I : Ideal S
J : Ideal R
⊢ J ∈ Ideal.minimalPrimes (comap f I) → J ∈ comap f '' Ideal.minimalPrimes I

case h.mpr
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J✝ : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
I : Ideal S
J : Ideal R
⊢ J ∈ comap f '' Ideal.minimalPrimes I → J ∈ Ideal.minimalPrimes (comap f I)
case h
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J✝ : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
I : Ideal S
J : Ideal R
⊢ J ∈ Ideal.minimalPrimes (comap f I) ↔ J ∈ comap f '' Ideal.minimalPrimes I
constructor
case h.mp
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J✝ : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
I : Ideal S
J : Ideal R
H : J ∈ Ideal.minimalPrimes (comap f I)
⊢ J ∈ comap f '' Ideal.minimalPrimes I
case h.mp
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J✝ : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
I : Ideal S
J : Ideal R
⊢ J ∈ Ideal.minimalPrimes (comap f I) → J ∈ comap f '' Ideal.minimalPrimes I
intro H
case h.mp.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
I p : Ideal S
h : p ∈ Ideal.minimalPrimes I
H : comap f p ∈ Ideal.minimalPrimes (comap f I)
⊢ comap f p ∈ comap f '' Ideal.minimalPrimes I
case h.mp
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J✝ : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
I : Ideal S
J : Ideal R
H : J ∈ Ideal.minimalPrimes (comap f I)
⊢ J ∈ comap f '' Ideal.minimalPrimes I
obtain ⟨p, h, rfl⟩ := Ideal.exists_minimalPrimes_comap_eq f J H
no goals
case h.mp.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
I p : Ideal S
h : p ∈ Ideal.minimalPrimes I
H : comap f p ∈ Ideal.minimalPrimes (comap f I)
⊢ comap f p ∈ comap f '' Ideal.minimalPrimes I
exact ⟨p, h, rfl⟩
case h.mpr.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J✝ : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
I J : Ideal S
hJ : J ∈ Ideal.minimalPrimes I
⊢ comap f J ∈ Ideal.minimalPrimes (comap f I)
case h.mpr
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J✝ : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
I : Ideal S
J : Ideal R
⊢ J ∈ comap f '' Ideal.minimalPrimes I → J ∈ Ideal.minimalPrimes (comap f I)
rintro ⟨J, hJ, rfl⟩
no goals
case h.mpr.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J✝ : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
I J : Ideal S
hJ : J ∈ Ideal.minimalPrimes I
⊢ comap f J ∈ Ideal.minimalPrimes (comap f I)
exact Ideal.mimimal_primes_comap_of_surjective hf hJ