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
h : J ∈ Ideal.minimalPrimes I
this : IsPrime J
⊢ comap f J ∈ Ideal.minimalPrimes (comap f 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 J : Ideal S
h : J ∈ Ideal.minimalPrimes I
⊢ comap f J ∈ Ideal.minimalPrimes (comap f I)
have := h.1.1
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
h : J ∈ Ideal.minimalPrimes I
this : IsPrime J
⊢ ∀ ⦃b : Ideal R⦄,
    b ∈ {p | IsPrime p ∧ comap f I ≤ p} → (fun x x_1 => x ≤ x_1) b (comap f J) → (fun x x_1 => x ≤ x_1) (comap f J) b
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
h : J ∈ Ideal.minimalPrimes I
this : IsPrime J
⊢ comap f J ∈ Ideal.minimalPrimes (comap f I)
refine' ⟨⟨inferInstance, Ideal.comap_mono h.1.2⟩, _⟩
case 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
h : J ∈ Ideal.minimalPrimes I
this : IsPrime J
K : Ideal R
hK : IsPrime K
e₁ : comap f I ≤ K
e₂ : K ≤ comap f J
⊢ comap f J ≤ K
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
h : J ∈ Ideal.minimalPrimes I
this : IsPrime J
⊢ ∀ ⦃b : Ideal R⦄,
    b ∈ {p | IsPrime p ∧ comap f I ≤ p} → (fun x x_1 => x ≤ x_1) b (comap f J) → (fun x x_1 => x ≤ x_1) (comap f J) b
rintro K ⟨hK, e₁⟩ e₂
case 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
h : J ∈ Ideal.minimalPrimes I
this✝ : IsPrime J
K : Ideal R
hK : IsPrime K
e₁ : comap f I ≤ K
e₂ : K ≤ comap f J
this : RingHom.ker f ≤ K
⊢ comap f J ≤ K
case 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
h : J ∈ Ideal.minimalPrimes I
this : IsPrime J
K : Ideal R
hK : IsPrime K
e₁ : comap f I ≤ K
e₂ : K ≤ comap f J
⊢ comap f J ≤ K
have : RingHom.ker f ≤ K := (Ideal.comap_mono bot_le).trans e₁
case 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
h : J ∈ Ideal.minimalPrimes I
this✝ : IsPrime J
K : Ideal R
hK : IsPrime K
e₁ : comap f I ≤ K
e₂ : K ≤ comap f J
this : RingHom.ker f ≤ K
⊢ comap f J ≤ comap f (map f K)
case 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
h : J ∈ Ideal.minimalPrimes I
this✝ : IsPrime J
K : Ideal R
hK : IsPrime K
e₁ : comap f I ≤ K
e₂ : K ≤ comap f J
this : RingHom.ker f ≤ K
⊢ comap f J ≤ K
rw [← sup_eq_left.mpr this, RingHom.ker_eq_comap_bot, ← Ideal.comap_map_of_surjective f hf]
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
h : J ∈ Ideal.minimalPrimes I
this✝ : IsPrime J
K : Ideal R
hK : IsPrime K
e₁ : comap f I ≤ K
e₂ : K ≤ comap f J
this : RingHom.ker f ≤ K
⊢ J ≤ map f K
case 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
h : J ∈ Ideal.minimalPrimes I
this✝ : IsPrime J
K : Ideal R
hK : IsPrime K
e₁ : comap f I ≤ K
e₂ : K ≤ comap f J
this : RingHom.ker f ≤ K
⊢ comap f J ≤ comap f (map f K)
apply Ideal.comap_mono _
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
h : J ∈ Ideal.minimalPrimes I
this✝ : IsPrime J
K : Ideal R
hK : IsPrime K
e₁ : comap f I ≤ K
e₂ : K ≤ comap f J
this : RingHom.ker f ≤ K
⊢ map f K ∈ {p | IsPrime p ∧ I ≤ p}

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
h : J ∈ Ideal.minimalPrimes I
this✝ : IsPrime J
K : Ideal R
hK : IsPrime K
e₁ : comap f I ≤ K
e₂ : K ≤ comap f J
this : RingHom.ker f ≤ K
⊢ map f K ≤ J
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
h : J ∈ Ideal.minimalPrimes I
this✝ : IsPrime J
K : Ideal R
hK : IsPrime K
e₁ : comap f I ≤ K
e₂ : K ≤ comap f J
this : RingHom.ker f ≤ K
⊢ J ≤ map f K
apply h.2 _ _
no goals
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
h : J ∈ Ideal.minimalPrimes I
this✝ : IsPrime J
K : Ideal R
hK : IsPrime K
e₁ : comap f I ≤ K
e₂ : K ≤ comap f J
this : RingHom.ker f ≤ K
⊢ map f K ∈ {p | IsPrime p ∧ I ≤ p}
exact ⟨Ideal.map_isPrime_of_surjective hf this, Ideal.le_map_of_comap_le_of_surjective f hf e₁⟩
no goals
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
h : J ∈ Ideal.minimalPrimes I
this✝ : IsPrime J
K : Ideal R
hK : IsPrime K
e₁ : comap f I ≤ K
e₂ : K ≤ comap f J
this : RingHom.ker f ≤ K
⊢ map f K ≤ J
exact Ideal.map_le_of_le_comap e₂