case map_nonunit
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝⁵ : CommRing R
inst✝⁴ : LocalRing R
inst✝³ : CommRing S
inst✝² : LocalRing S
inst✝¹ : CommRing T
inst✝ : LocalRing T
⊢ ∀ (a : R), IsUnit (↑(residue R) a) → IsUnit a
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝⁵ : CommRing R
inst✝⁴ : LocalRing R
inst✝³ : CommRing S
inst✝² : LocalRing S
inst✝¹ : CommRing T
inst✝ : LocalRing T
⊢ IsLocalRingHom (residue R)
constructor
case map_nonunit
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝⁵ : CommRing R
inst✝⁴ : LocalRing R
inst✝³ : CommRing S
inst✝² : LocalRing S
inst✝¹ : CommRing T
inst✝ : LocalRing T
a : R
ha : IsUnit (↑(residue R) a)
⊢ IsUnit a
case map_nonunit
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝⁵ : CommRing R
inst✝⁴ : LocalRing R
inst✝³ : CommRing S
inst✝² : LocalRing S
inst✝¹ : CommRing T
inst✝ : LocalRing T
⊢ ∀ (a : R), IsUnit (↑(residue R) a) → IsUnit a
intro a ha
case map_nonunit
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝⁵ : CommRing R
inst✝⁴ : LocalRing R
inst✝³ : CommRing S
inst✝² : LocalRing S
inst✝¹ : CommRing T
inst✝ : LocalRing T
a : R
ha : IsUnit (↑(residue R) a)
h : ¬IsUnit a
⊢ False
case map_nonunit
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝⁵ : CommRing R
inst✝⁴ : LocalRing R
inst✝³ : CommRing S
inst✝² : LocalRing S
inst✝¹ : CommRing T
inst✝ : LocalRing T
a : R
ha : IsUnit (↑(residue R) a)
⊢ IsUnit a
by_contra h
case map_nonunit
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝⁵ : CommRing R
inst✝⁴ : LocalRing R
inst✝³ : CommRing S
inst✝² : LocalRing S
inst✝¹ : CommRing T
inst✝ : LocalRing T
a : R
ha : IsUnit 0
h : ¬IsUnit a
⊢ False
case map_nonunit
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝⁵ : CommRing R
inst✝⁴ : LocalRing R
inst✝³ : CommRing S
inst✝² : LocalRing S
inst✝¹ : CommRing T
inst✝ : LocalRing T
a : R
ha : IsUnit (↑(residue R) a)
h : ¬IsUnit a
⊢ False
erw [Ideal.Quotient.eq_zero_iff_mem.mpr ((LocalRing.mem_maximalIdeal _).mpr h)] at ha
no goals
case map_nonunit
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝⁵ : CommRing R
inst✝⁴ : LocalRing R
inst✝³ : CommRing S
inst✝² : LocalRing S
inst✝¹ : CommRing T
inst✝ : LocalRing T
a : R
ha : IsUnit 0
h : ¬IsUnit a
⊢ False
exact ha.ne_zero rfl