case map_nonunit
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I ≤ Ideal.jacobson ⊥
⊢ ∀ (a : R), IsUnit (↑(Ideal.Quotient.mk I) a) → IsUnit a
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I ≤ Ideal.jacobson ⊥
⊢ IsLocalRingHom (Ideal.Quotient.mk I)
constructor
case map_nonunit
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h✝ : I ≤ Ideal.jacobson ⊥
a : R
h : IsUnit (↑(Ideal.Quotient.mk I) a)
⊢ IsUnit a
case map_nonunit
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I ≤ Ideal.jacobson ⊥
⊢ ∀ (a : R), IsUnit (↑(Ideal.Quotient.mk I) a) → IsUnit a
intro a h
case map_nonunit
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h✝ : I ≤ Ideal.jacobson ⊥
a : R
h : IsUnit (↑(Ideal.Quotient.mk I) a)
this : IsUnit (↑(Ideal.Quotient.mk (Ideal.jacobson ⊥)) a)
⊢ IsUnit a
case map_nonunit
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h✝ : I ≤ Ideal.jacobson ⊥
a : R
h : IsUnit (↑(Ideal.Quotient.mk I) a)
⊢ IsUnit a
have : IsUnit (Ideal.Quotient.mk (Ideal.jacobson ⊥) a) := by
  rw [isUnit_iff_exists_inv] at *
  obtain ⟨b, hb⟩ := h
  obtain ⟨b, rfl⟩ := Ideal.Quotient.mk_surjective b
  use Ideal.Quotient.mk _ b
  rw [← (Ideal.Quotient.mk _).map_one, ← (Ideal.Quotient.mk _).map_mul, Ideal.Quotient.eq] at hb⊢
  exact h hb
case map_nonunit.intro.mk
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h✝ : I ≤ Ideal.jacobson ⊥
a : R
h : IsUnit (↑(Ideal.Quotient.mk I) a)
y : R ⧸ Ideal.jacobson ⊥
h1 : ↑(Ideal.Quotient.mk (Ideal.jacobson ⊥)) a * y = 1
h2 : y * ↑(Ideal.Quotient.mk (Ideal.jacobson ⊥)) a = 1
⊢ IsUnit a
case map_nonunit
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h✝ : I ≤ Ideal.jacobson ⊥
a : R
h : IsUnit (↑(Ideal.Quotient.mk I) a)
this : IsUnit (↑(Ideal.Quotient.mk (Ideal.jacobson ⊥)) a)
⊢ IsUnit a
obtain ⟨⟨x, y, h1, h2⟩, rfl : x = _⟩ := this
case map_nonunit.intro.mk.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h✝ : I ≤ Ideal.jacobson ⊥
a : R
h : IsUnit (↑(Ideal.Quotient.mk I) a)
y : R
h1 : ↑(Ideal.Quotient.mk (Ideal.jacobson ⊥)) a * ↑(Ideal.Quotient.mk (Ideal.jacobson ⊥)) y = 1
h2 : ↑(Ideal.Quotient.mk (Ideal.jacobson ⊥)) y * ↑(Ideal.Quotient.mk (Ideal.jacobson ⊥)) a = 1
⊢ IsUnit a
case map_nonunit.intro.mk
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h✝ : I ≤ Ideal.jacobson ⊥
a : R
h : IsUnit (↑(Ideal.Quotient.mk I) a)
y : R ⧸ Ideal.jacobson ⊥
h1 : ↑(Ideal.Quotient.mk (Ideal.jacobson ⊥)) a * y = 1
h2 : y * ↑(Ideal.Quotient.mk (Ideal.jacobson ⊥)) a = 1
⊢ IsUnit a
obtain ⟨y, rfl⟩ := Ideal.Quotient.mk_surjective y
case map_nonunit.intro.mk.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h✝ : I ≤ Ideal.jacobson ⊥
a : R
h : IsUnit (↑(Ideal.Quotient.mk I) a)
y : R
h1 : ∀ (y_1 : R), IsUnit ((a * y - 1) * y_1 + 1)
h2 : ∀ (y_1 : R), IsUnit ((y * a - 1) * y_1 + 1)
⊢ IsUnit a
case map_nonunit.intro.mk.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h✝ : I ≤ Ideal.jacobson ⊥
a : R
h : IsUnit (↑(Ideal.Quotient.mk I) a)
y : R
h1 : ↑(Ideal.Quotient.mk (Ideal.jacobson ⊥)) a * ↑(Ideal.Quotient.mk (Ideal.jacobson ⊥)) y = 1
h2 : ↑(Ideal.Quotient.mk (Ideal.jacobson ⊥)) y * ↑(Ideal.Quotient.mk (Ideal.jacobson ⊥)) a = 1
⊢ IsUnit a
rw [← (Ideal.Quotient.mk _).map_mul, ← (Ideal.Quotient.mk _).map_one, Ideal.Quotient.eq,
  Ideal.mem_jacobson_bot] at h1 h2
case map_nonunit.intro.mk.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h✝ : I ≤ Ideal.jacobson ⊥
a : R
h : IsUnit (↑(Ideal.Quotient.mk I) a)
y : R
h2 : ∀ (y_1 : R), IsUnit ((y * a - 1) * y_1 + 1)
h1 : IsUnit ((a * y - 1) * 1 + 1)
⊢ IsUnit a
case map_nonunit.intro.mk.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h✝ : I ≤ Ideal.jacobson ⊥
a : R
h : IsUnit (↑(Ideal.Quotient.mk I) a)
y : R
h1 : ∀ (y_1 : R), IsUnit ((a * y - 1) * y_1 + 1)
h2 : ∀ (y_1 : R), IsUnit ((y * a - 1) * y_1 + 1)
⊢ IsUnit a
specialize h1 1
case map_nonunit.intro.mk.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h✝ : I ≤ Ideal.jacobson ⊥
a : R
h : IsUnit (↑(Ideal.Quotient.mk I) a)
y : R
h2 : ∀ (y_1 : R), IsUnit ((y * a - 1) * y_1 + 1)
h1 : IsUnit a ∧ IsUnit y
⊢ IsUnit a
case map_nonunit.intro.mk.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h✝ : I ≤ Ideal.jacobson ⊥
a : R
h : IsUnit (↑(Ideal.Quotient.mk I) a)
y : R
h2 : ∀ (y_1 : R), IsUnit ((y * a - 1) * y_1 + 1)
h1 : IsUnit ((a * y - 1) * 1 + 1)
⊢ IsUnit a
simp at h1
no goals
case map_nonunit.intro.mk.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h✝ : I ≤ Ideal.jacobson ⊥
a : R
h : IsUnit (↑(Ideal.Quotient.mk I) a)
y : R
h2 : ∀ (y_1 : R), IsUnit ((y * a - 1) * y_1 + 1)
h1 : IsUnit a ∧ IsUnit y
⊢ IsUnit a
exact h1.1
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h✝ : I ≤ Ideal.jacobson ⊥
a : R
h : ∃ b, ↑(Ideal.Quotient.mk I) a * b = 1
⊢ ∃ b, ↑(Ideal.Quotient.mk (Ideal.jacobson ⊥)) a * b = 1
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h✝ : I ≤ Ideal.jacobson ⊥
a : R
h : IsUnit (↑(Ideal.Quotient.mk I) a)
⊢ IsUnit (↑(Ideal.Quotient.mk (Ideal.jacobson ⊥)) a)
rw [isUnit_iff_exists_inv] at *
case intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I ≤ Ideal.jacobson ⊥
a : R
b : R ⧸ I
hb : ↑(Ideal.Quotient.mk I) a * b = 1
⊢ ∃ b, ↑(Ideal.Quotient.mk (Ideal.jacobson ⊥)) a * b = 1
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h✝ : I ≤ Ideal.jacobson ⊥
a : R
h : ∃ b, ↑(Ideal.Quotient.mk I) a * b = 1
⊢ ∃ b, ↑(Ideal.Quotient.mk (Ideal.jacobson ⊥)) a * b = 1
obtain ⟨b, hb⟩ := h
case intro.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I ≤ Ideal.jacobson ⊥
a b : R
hb : ↑(Ideal.Quotient.mk I) a * ↑(Ideal.Quotient.mk I) b = 1
⊢ ∃ b, ↑(Ideal.Quotient.mk (Ideal.jacobson ⊥)) a * b = 1
case intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I ≤ Ideal.jacobson ⊥
a : R
b : R ⧸ I
hb : ↑(Ideal.Quotient.mk I) a * b = 1
⊢ ∃ b, ↑(Ideal.Quotient.mk (Ideal.jacobson ⊥)) a * b = 1
obtain ⟨b, rfl⟩ := Ideal.Quotient.mk_surjective b
case intro.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I ≤ Ideal.jacobson ⊥
a b : R
hb : ↑(Ideal.Quotient.mk I) a * ↑(Ideal.Quotient.mk I) b = 1
⊢ ↑(Ideal.Quotient.mk (Ideal.jacobson ⊥)) a * ↑(Ideal.Quotient.mk (Ideal.jacobson ⊥)) b = 1
case intro.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I ≤ Ideal.jacobson ⊥
a b : R
hb : ↑(Ideal.Quotient.mk I) a * ↑(Ideal.Quotient.mk I) b = 1
⊢ ∃ b, ↑(Ideal.Quotient.mk (Ideal.jacobson ⊥)) a * b = 1
use Ideal.Quotient.mk _ b
case intro.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I ≤ Ideal.jacobson ⊥
a b : R
hb : a * b - 1 ∈ I
⊢ a * b - 1 ∈ Ideal.jacobson ⊥
case intro.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I ≤ Ideal.jacobson ⊥
a b : R
hb : ↑(Ideal.Quotient.mk I) a * ↑(Ideal.Quotient.mk I) b = 1
⊢ ↑(Ideal.Quotient.mk (Ideal.jacobson ⊥)) a * ↑(Ideal.Quotient.mk (Ideal.jacobson ⊥)) b = 1
rw [← (Ideal.Quotient.mk _).map_one, ← (Ideal.Quotient.mk _).map_mul, Ideal.Quotient.eq] at hb⊢
no goals
case intro.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I ≤ Ideal.jacobson ⊥
a b : R
hb : a * b - 1 ∈ I
⊢ a * b - 1 ∈ Ideal.jacobson ⊥
exact h hb