R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f✝ : R →+* S
I : Ideal R
f : R →+* S
H : ∀ (a : R), a ∈ I → ↑f a = 0
hI : ker f ≤ I
⊢ ∀ (x : R ⧸ I), ↑(Ideal.Quotient.lift I f H) x = 0 → x = 0
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f✝ : R →+* S
I : Ideal R
f : R →+* S
H : ∀ (a : R), a ∈ I → ↑f a = 0
hI : ker f ≤ I
⊢ Function.Injective ↑(Ideal.Quotient.lift I f H)
rw [RingHom.injective_iff_ker_eq_bot, RingHom.ker_eq_bot_iff_eq_zero]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f✝ : R →+* S
I : Ideal R
f : R →+* S
H : ∀ (a : R), a ∈ I → ↑f a = 0
hI : ker f ≤ I
u : R ⧸ I
hu : ↑(Ideal.Quotient.lift I f H) u = 0
⊢ u = 0
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f✝ : R →+* S
I : Ideal R
f : R →+* S
H : ∀ (a : R), a ∈ I → ↑f a = 0
hI : ker f ≤ I
⊢ ∀ (x : R ⧸ I), ↑(Ideal.Quotient.lift I f H) x = 0 → x = 0
intro u hu
case intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f✝ : R →+* S
I : Ideal R
f : R →+* S
H : ∀ (a : R), a ∈ I → ↑f a = 0
hI : ker f ≤ I
v : R
hu : ↑(Ideal.Quotient.lift I f H) (↑(Ideal.Quotient.mk I) v) = 0
⊢ ↑(Ideal.Quotient.mk I) v = 0
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f✝ : R →+* S
I : Ideal R
f : R →+* S
H : ∀ (a : R), a ∈ I → ↑f a = 0
hI : ker f ≤ I
u : R ⧸ I
hu : ↑(Ideal.Quotient.lift I f H) u = 0
⊢ u = 0
obtain ⟨v, rfl⟩ := Ideal.Quotient.mk_surjective u
case intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f✝ : R →+* S
I : Ideal R
f : R →+* S
H : ∀ (a : R), a ∈ I → ↑f a = 0
hI : ker f ≤ I
v : R
hu : ↑f v = 0
⊢ ↑(Ideal.Quotient.mk I) v = 0
case intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f✝ : R →+* S
I : Ideal R
f : R →+* S
H : ∀ (a : R), a ∈ I → ↑f a = 0
hI : ker f ≤ I
v : R
hu : ↑(Ideal.Quotient.lift I f H) (↑(Ideal.Quotient.mk I) v) = 0
⊢ ↑(Ideal.Quotient.mk I) v = 0
rw [Ideal.Quotient.lift_mk] at hu
case intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f✝ : R →+* S
I : Ideal R
f : R →+* S
H : ∀ (a : R), a ∈ I → ↑f a = 0
hI : ker f ≤ I
v : R
hu : ↑f v = 0
⊢ v ∈ I
case intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f✝ : R →+* S
I : Ideal R
f : R →+* S
H : ∀ (a : R), a ∈ I → ↑f a = 0
hI : ker f ≤ I
v : R
hu : ↑f v = 0
⊢ ↑(Ideal.Quotient.mk I) v = 0
rw [Ideal.Quotient.eq_zero_iff_mem]
no goals
case intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f✝ : R →+* S
I : Ideal R
f : R →+* S
H : ∀ (a : R), a ∈ I → ↑f a = 0
hI : ker f ≤ I
v : R
hu : ↑f v = 0
⊢ v ∈ I
exact hI ((RingHom.mem_ker f).mpr hu)