R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type ?u.1390678
R₂ : Type ?u.1390681
A : Type ?u.1390684
B : Type ?u.1390687
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
J : Ideal R
I : Ideal S
f : R →+* S
H : J ≤ comap f I
h : comap f I ≤ J
a : R ⧸ J
ha : ↑(quotientMap I f H) a = 0
⊢ a = 0
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type ?u.1390678
R₂ : Type ?u.1390681
A : Type ?u.1390684
B : Type ?u.1390687
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
J : Ideal R
I : Ideal S
f : R →+* S
H : J ≤ comap f I
h : comap f I ≤ J
⊢ Function.Injective ↑(quotientMap I f H)
refine' (injective_iff_map_eq_zero (quotientMap I f H)).2 fun a ha => _
case intro
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type ?u.1390678
R₂ : Type ?u.1390681
A : Type ?u.1390684
B : Type ?u.1390687
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
J : Ideal R
I : Ideal S
f : R →+* S
H : J ≤ comap f I
h : comap f I ≤ J
r : R
ha : ↑(quotientMap I f H) (↑(Quotient.mk J) r) = 0
⊢ ↑(Quotient.mk J) r = 0
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type ?u.1390678
R₂ : Type ?u.1390681
A : Type ?u.1390684
B : Type ?u.1390687
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
J : Ideal R
I : Ideal S
f : R →+* S
H : J ≤ comap f I
h : comap f I ≤ J
a : R ⧸ J
ha : ↑(quotientMap I f H) a = 0
⊢ a = 0
obtain ⟨r, rfl⟩ := Quotient.mk_surjective a
case intro
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type ?u.1390678
R₂ : Type ?u.1390681
A : Type ?u.1390684
B : Type ?u.1390687
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
J : Ideal R
I : Ideal S
f : R →+* S
H : J ≤ comap f I
h : comap f I ≤ J
r : R
ha : ↑f r ∈ I
⊢ ↑(Quotient.mk J) r = 0
case intro
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type ?u.1390678
R₂ : Type ?u.1390681
A : Type ?u.1390684
B : Type ?u.1390687
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
J : Ideal R
I : Ideal S
f : R →+* S
H : J ≤ comap f I
h : comap f I ≤ J
r : R
ha : ↑(quotientMap I f H) (↑(Quotient.mk J) r) = 0
⊢ ↑(Quotient.mk J) r = 0
rw [quotientMap_mk, Quotient.eq_zero_iff_mem] at ha
no goals
case intro
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type ?u.1390678
R₂ : Type ?u.1390681
A : Type ?u.1390684
B : Type ?u.1390687
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
J : Ideal R
I : Ideal S
f : R →+* S
H : J ≤ comap f I
h : comap f I ≤ J
r : R
ha : ↑f r ∈ I
⊢ ↑(Quotient.mk J) r = 0
exact Quotient.eq_zero_iff_mem.mpr (h ha)