[GOAL]
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝ : CommSemiring R
h : ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
⊢ ∃! I, Ideal.IsMaximal I
[PROOFSTEP]
rcases h with ⟨P, ⟨hPnonzero, hPnot_top, _⟩, hPunique⟩
[GOAL]
case intro.intro.intro.mk
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝ : CommSemiring R
P : Ideal R
hPunique : ∀ (y : Ideal R), (fun P => P ≠ ⊥ ∧ Ideal.IsPrime P) y → y = P
hPnonzero : P ≠ ⊥
hPnot_top : P ≠ ⊤
mem_or_mem'✝ : ∀ {x y : R}, x * y ∈ P → x ∈ P ∨ y ∈ P
⊢ ∃! I, Ideal.IsMaximal I
[PROOFSTEP]
refine' ⟨P, ⟨⟨hPnot_top, _⟩⟩, fun M hM => hPunique _ ⟨_, Ideal.IsMaximal.isPrime hM⟩⟩
[GOAL]
case intro.intro.intro.mk.refine'_1
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝ : CommSemiring R
P : Ideal R
hPunique : ∀ (y : Ideal R), (fun P => P ≠ ⊥ ∧ Ideal.IsPrime P) y → y = P
hPnonzero : P ≠ ⊥
hPnot_top : P ≠ ⊤
mem_or_mem'✝ : ∀ {x y : R}, x * y ∈ P → x ∈ P ∨ y ∈ P
⊢ ∀ (b : Ideal R), P < b → b = ⊤
[PROOFSTEP]
refine' Ideal.maximal_of_no_maximal fun M hPM hM => ne_of_lt hPM _
[GOAL]
case intro.intro.intro.mk.refine'_1
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝ : CommSemiring R
P : Ideal R
hPunique : ∀ (y : Ideal R), (fun P => P ≠ ⊥ ∧ Ideal.IsPrime P) y → y = P
hPnonzero : P ≠ ⊥
hPnot_top : P ≠ ⊤
mem_or_mem'✝ : ∀ {x y : R}, x * y ∈ P → x ∈ P ∨ y ∈ P
M : Ideal R
hPM : P < M
hM : Ideal.IsMaximal M
⊢ P = M
[PROOFSTEP]
exact (hPunique _ ⟨ne_bot_of_gt hPM, Ideal.IsMaximal.isPrime hM⟩).symm
[GOAL]
case intro.intro.intro.mk.refine'_2
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝ : CommSemiring R
P : Ideal R
hPunique : ∀ (y : Ideal R), (fun P => P ≠ ⊥ ∧ Ideal.IsPrime P) y → y = P
hPnonzero : P ≠ ⊥
hPnot_top : P ≠ ⊤
mem_or_mem'✝ : ∀ {x y : R}, x * y ∈ P → x ∈ P ∨ y ∈ P
M : Ideal R
hM : (fun I => Ideal.IsMaximal I) M
⊢ M ≠ ⊥
[PROOFSTEP]
rintro rfl
[GOAL]
case intro.intro.intro.mk.refine'_2
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝ : CommSemiring R
P : Ideal R
hPunique : ∀ (y : Ideal R), (fun P => P ≠ ⊥ ∧ Ideal.IsPrime P) y → y = P
hPnonzero : P ≠ ⊥
hPnot_top : P ≠ ⊤
mem_or_mem'✝ : ∀ {x y : R}, x * y ∈ P → x ∈ P ∨ y ∈ P
hM : Ideal.IsMaximal ⊥
⊢ False
[PROOFSTEP]
exact hPnot_top (hM.1.2 P (bot_lt_iff_ne_bot.2 hPnonzero))
[GOAL]
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommSemiring R
inst✝ : LocalRing R
a b : R
h : IsUnit (a + b)
⊢ IsUnit a ∨ IsUnit b
[PROOFSTEP]
rcases h with ⟨u, hu⟩
[GOAL]
case intro
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommSemiring R
inst✝ : LocalRing R
a b : R
u : Rˣ
hu : ↑u = a + b
⊢ IsUnit a ∨ IsUnit b
[PROOFSTEP]
rw [← Units.inv_mul_eq_one, mul_add] at hu 
[GOAL]
case intro
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommSemiring R
inst✝ : LocalRing R
a b : R
u : Rˣ
hu : ↑u⁻¹ * a + ↑u⁻¹ * b = 1
⊢ IsUnit a ∨ IsUnit b
[PROOFSTEP]
apply Or.imp _ _ (isUnit_or_isUnit_of_add_one hu)
[GOAL]
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommSemiring R
inst✝ : LocalRing R
a b : R
u : Rˣ
hu : ↑u⁻¹ * a + ↑u⁻¹ * b = 1
⊢ IsUnit (↑u⁻¹ * a) → IsUnit a
[PROOFSTEP]
exact isUnit_of_mul_isUnit_right
[GOAL]
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommSemiring R
inst✝ : LocalRing R
a b : R
u : Rˣ
hu : ↑u⁻¹ * a + ↑u⁻¹ * b = 1
⊢ IsUnit (↑u⁻¹ * b) → IsUnit b
[PROOFSTEP]
exact isUnit_of_mul_isUnit_right
[GOAL]
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommSemiring R
inst✝ : LocalRing R
⊢ Ideal.IsMaximal (maximalIdeal R)
[PROOFSTEP]
rw [Ideal.isMaximal_iff]
[GOAL]
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommSemiring R
inst✝ : LocalRing R
⊢ ¬1 ∈ maximalIdeal R ∧ ∀ (J : Ideal R) (x : R), maximalIdeal R ≤ J → ¬x ∈ maximalIdeal R → x ∈ J → 1 ∈ J
[PROOFSTEP]
constructor
[GOAL]
case left
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommSemiring R
inst✝ : LocalRing R
⊢ ¬1 ∈ maximalIdeal R
[PROOFSTEP]
intro h
[GOAL]
case left
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommSemiring R
inst✝ : LocalRing R
h : 1 ∈ maximalIdeal R
⊢ False
[PROOFSTEP]
apply h
[GOAL]
case left
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommSemiring R
inst✝ : LocalRing R
h : 1 ∈ maximalIdeal R
⊢ IsUnit 1
[PROOFSTEP]
exact isUnit_one
[GOAL]
case right
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommSemiring R
inst✝ : LocalRing R
⊢ ∀ (J : Ideal R) (x : R), maximalIdeal R ≤ J → ¬x ∈ maximalIdeal R → x ∈ J → 1 ∈ J
[PROOFSTEP]
intro I x _ hx H
[GOAL]
case right
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommSemiring R
inst✝ : LocalRing R
I : Ideal R
x : R
a✝ : maximalIdeal R ≤ I
hx : ¬x ∈ maximalIdeal R
H : x ∈ I
⊢ 1 ∈ I
[PROOFSTEP]
erw [Classical.not_not] at hx 
[GOAL]
case right
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommSemiring R
inst✝ : LocalRing R
I : Ideal R
x : R
a✝ : maximalIdeal R ≤ I
hx : IsUnit x
H : x ∈ I
⊢ 1 ∈ I
[PROOFSTEP]
rcases hx with ⟨u, rfl⟩
[GOAL]
case right.intro
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommSemiring R
inst✝ : LocalRing R
I : Ideal R
a✝ : maximalIdeal R ≤ I
u : Rˣ
H : ↑u ∈ I
⊢ 1 ∈ I
[PROOFSTEP]
simpa using I.mul_mem_left (↑u⁻¹) H
[GOAL]
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommSemiring R
inst✝ : LocalRing R
J : Ideal R
hJ : J ≠ ⊤
⊢ J ≤ maximalIdeal R
[PROOFSTEP]
rcases Ideal.exists_le_maximal J hJ with ⟨M, hM1, hM2⟩
[GOAL]
case intro.intro
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommSemiring R
inst✝ : LocalRing R
J : Ideal R
hJ : J ≠ ⊤
M : Ideal R
hM1 : Ideal.IsMaximal M
hM2 : J ≤ M
⊢ J ≤ maximalIdeal R
[PROOFSTEP]
rwa [← eq_maximalIdeal hM1]
[GOAL]
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝³ : CommRing R
inst✝² : LocalRing R
inst✝¹ : CommRing S
inst✝ : Nontrivial S
f : R →+* S
hf : Function.Surjective ↑f
⊢ ∀ (a : S), IsUnit a ∨ IsUnit (1 - a)
[PROOFSTEP]
intro b
[GOAL]
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝³ : CommRing R
inst✝² : LocalRing R
inst✝¹ : CommRing S
inst✝ : Nontrivial S
f : R →+* S
hf : Function.Surjective ↑f
b : S
⊢ IsUnit b ∨ IsUnit (1 - b)
[PROOFSTEP]
obtain ⟨a, rfl⟩ := hf b
[GOAL]
case intro
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝³ : CommRing R
inst✝² : LocalRing R
inst✝¹ : CommRing S
inst✝ : Nontrivial S
f : R →+* S
hf : Function.Surjective ↑f
a : R
⊢ IsUnit (↑f a) ∨ IsUnit (1 - ↑f a)
[PROOFSTEP]
apply (isUnit_or_isUnit_one_sub_self a).imp <| RingHom.isUnit_map _
[GOAL]
case intro
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝³ : CommRing R
inst✝² : LocalRing R
inst✝¹ : CommRing S
inst✝ : Nontrivial S
f : R →+* S
hf : Function.Surjective ↑f
a : R
⊢ IsUnit (1 - a) → IsUnit (1 - ↑f a)
[PROOFSTEP]
rw [← f.map_one, ← f.map_sub]
[GOAL]
case intro
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝³ : CommRing R
inst✝² : LocalRing R
inst✝¹ : CommRing S
inst✝ : Nontrivial S
f : R →+* S
hf : Function.Surjective ↑f
a : R
⊢ IsUnit (1 - a) → IsUnit (↑f (1 - a))
[PROOFSTEP]
apply f.isUnit_map
[GOAL]
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommRing R
inst✝ : LocalRing R
I : Ideal R
h : I ≠ ⊤
⊢ Ideal.jacobson I = maximalIdeal R
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommRing R
inst✝ : LocalRing R
I : Ideal R
h : I ≠ ⊤
⊢ Ideal.jacobson I ≤ maximalIdeal R
[PROOFSTEP]
exact sInf_le ⟨LocalRing.le_maximalIdeal h, LocalRing.maximalIdeal.isMaximal R⟩
[GOAL]
case a
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommRing R
inst✝ : LocalRing R
I : Ideal R
h : I ≠ ⊤
⊢ maximalIdeal R ≤ Ideal.jacobson I
[PROOFSTEP]
exact le_sInf fun J (hJ : I ≤ J ∧ J.IsMaximal) => le_of_eq (LocalRing.eq_maximalIdeal hJ.2).symm
[GOAL]
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Semiring T
f : R ≃+* S
a : R
ha : IsUnit (↑↑f a)
⊢ IsUnit a
[PROOFSTEP]
convert RingHom.isUnit_map (f.symm : S →+* R) ha
[GOAL]
case h.e'_3
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Semiring T
f : R ≃+* S
a : R
ha : IsUnit (↑↑f a)
⊢ a = ↑↑(RingEquiv.symm f) (↑↑f a)
[PROOFSTEP]
exact (RingEquiv.symm_apply_apply f a).symm
[GOAL]
R✝ : Type u
S✝ : Type v
T : Type w
K : Type u'
inst✝⁵ : Semiring R✝
inst✝⁴ : Semiring S✝
inst✝³ : Semiring T
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
H : LocalRing S
f : R →+* S
inst✝ : IsLocalRingHom f
⊢ LocalRing R
[PROOFSTEP]
haveI : Nontrivial R := pullback_nonzero f f.map_zero f.map_one
[GOAL]
R✝ : Type u
S✝ : Type v
T : Type w
K : Type u'
inst✝⁵ : Semiring R✝
inst✝⁴ : Semiring S✝
inst✝³ : Semiring T
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
H : LocalRing S
f : R →+* S
inst✝ : IsLocalRingHom f
this : Nontrivial R
⊢ LocalRing R
[PROOFSTEP]
apply LocalRing.of_nonunits_add
[GOAL]
case h
R✝ : Type u
S✝ : Type v
T : Type w
K : Type u'
inst✝⁵ : Semiring R✝
inst✝⁴ : Semiring S✝
inst✝³ : Semiring T
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
H : LocalRing S
f : R →+* S
inst✝ : IsLocalRingHom f
this : Nontrivial R
⊢ ∀ (a b : R), a ∈ nonunits R → b ∈ nonunits R → a + b ∈ nonunits R
[PROOFSTEP]
intro a b
[GOAL]
case h
R✝ : Type u
S✝ : Type v
T : Type w
K : Type u'
inst✝⁵ : Semiring R✝
inst✝⁴ : Semiring S✝
inst✝³ : Semiring T
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
H : LocalRing S
f : R →+* S
inst✝ : IsLocalRingHom f
this : Nontrivial R
a b : R
⊢ a ∈ nonunits R → b ∈ nonunits R → a + b ∈ nonunits R
[PROOFSTEP]
simp_rw [← map_mem_nonunits_iff f, f.map_add]
[GOAL]
case h
R✝ : Type u
S✝ : Type v
T : Type w
K : Type u'
inst✝⁵ : Semiring R✝
inst✝⁴ : Semiring S✝
inst✝³ : Semiring T
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
H : LocalRing S
f : R →+* S
inst✝ : IsLocalRingHom f
this : Nontrivial R
a b : R
⊢ ↑f a ∈ nonunits S → ↑f b ∈ nonunits S → ↑f a + ↑f b ∈ nonunits S
[PROOFSTEP]
exact LocalRing.nonunits_add
[GOAL]
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝³ : CommSemiring R
inst✝² : LocalRing R
inst✝¹ : CommSemiring S
inst✝ : LocalRing S
f : R →+* S
⊢ List.TFAE
    [IsLocalRingHom f, ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S),
      Ideal.map f (maximalIdeal R) ≤ maximalIdeal S, maximalIdeal R ≤ Ideal.comap f (maximalIdeal S),
      Ideal.comap f (maximalIdeal S) = maximalIdeal R]
[PROOFSTEP]
tfae_have 1 → 2
[GOAL]
case tfae_1_to_2
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝³ : CommSemiring R
inst✝² : LocalRing R
inst✝¹ : CommSemiring S
inst✝ : LocalRing S
f : R →+* S
⊢ IsLocalRingHom f → ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S)
[PROOFSTEP]
rintro _ _ ⟨a, ha, rfl⟩
[GOAL]
case tfae_1_to_2.intro.intro
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝³ : CommSemiring R
inst✝² : LocalRing R
inst✝¹ : CommSemiring S
inst✝ : LocalRing S
f : R →+* S
✝ : IsLocalRingHom f
a : R
ha : a ∈ ↑(maximalIdeal R).toAddSubmonoid
⊢ ↑f a ∈ ↑(maximalIdeal S)
[PROOFSTEP]
exact map_nonunit f a ha
[GOAL]
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝³ : CommSemiring R
inst✝² : LocalRing R
inst✝¹ : CommSemiring S
inst✝ : LocalRing S
f : R →+* S
tfae_1_to_2 : IsLocalRingHom f → ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S)
⊢ List.TFAE
    [IsLocalRingHom f, ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S),
      Ideal.map f (maximalIdeal R) ≤ maximalIdeal S, maximalIdeal R ≤ Ideal.comap f (maximalIdeal S),
      Ideal.comap f (maximalIdeal S) = maximalIdeal R]
[PROOFSTEP]
tfae_have 2 → 4
[GOAL]
case tfae_2_to_4
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝³ : CommSemiring R
inst✝² : LocalRing R
inst✝¹ : CommSemiring S
inst✝ : LocalRing S
f : R →+* S
tfae_1_to_2 : IsLocalRingHom f → ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S)
⊢ ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S) → maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
[PROOFSTEP]
exact Set.image_subset_iff.1
[GOAL]
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝³ : CommSemiring R
inst✝² : LocalRing R
inst✝¹ : CommSemiring S
inst✝ : LocalRing S
f : R →+* S
tfae_1_to_2 : IsLocalRingHom f → ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S)
tfae_2_to_4 :
  ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S) → maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
⊢ List.TFAE
    [IsLocalRingHom f, ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S),
      Ideal.map f (maximalIdeal R) ≤ maximalIdeal S, maximalIdeal R ≤ Ideal.comap f (maximalIdeal S),
      Ideal.comap f (maximalIdeal S) = maximalIdeal R]
[PROOFSTEP]
tfae_have 3 ↔ 4
[GOAL]
case tfae_3_iff_4
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝³ : CommSemiring R
inst✝² : LocalRing R
inst✝¹ : CommSemiring S
inst✝ : LocalRing S
f : R →+* S
tfae_1_to_2 : IsLocalRingHom f → ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S)
tfae_2_to_4 :
  ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S) → maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
⊢ Ideal.map f (maximalIdeal R) ≤ maximalIdeal S ↔ maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
[PROOFSTEP]
exact Ideal.map_le_iff_le_comap
[GOAL]
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝³ : CommSemiring R
inst✝² : LocalRing R
inst✝¹ : CommSemiring S
inst✝ : LocalRing S
f : R →+* S
tfae_1_to_2 : IsLocalRingHom f → ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S)
tfae_2_to_4 :
  ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S) → maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_3_iff_4 : Ideal.map f (maximalIdeal R) ≤ maximalIdeal S ↔ maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
⊢ List.TFAE
    [IsLocalRingHom f, ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S),
      Ideal.map f (maximalIdeal R) ≤ maximalIdeal S, maximalIdeal R ≤ Ideal.comap f (maximalIdeal S),
      Ideal.comap f (maximalIdeal S) = maximalIdeal R]
[PROOFSTEP]
tfae_have 4 → 1
[GOAL]
case tfae_4_to_1
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝³ : CommSemiring R
inst✝² : LocalRing R
inst✝¹ : CommSemiring S
inst✝ : LocalRing S
f : R →+* S
tfae_1_to_2 : IsLocalRingHom f → ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S)
tfae_2_to_4 :
  ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S) → maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_3_iff_4 : Ideal.map f (maximalIdeal R) ≤ maximalIdeal S ↔ maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
⊢ maximalIdeal R ≤ Ideal.comap f (maximalIdeal S) → IsLocalRingHom f
[PROOFSTEP]
intro h
[GOAL]
case tfae_4_to_1
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝³ : CommSemiring R
inst✝² : LocalRing R
inst✝¹ : CommSemiring S
inst✝ : LocalRing S
f : R →+* S
tfae_1_to_2 : IsLocalRingHom f → ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S)
tfae_2_to_4 :
  ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S) → maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_3_iff_4 : Ideal.map f (maximalIdeal R) ≤ maximalIdeal S ↔ maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
h : maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
⊢ IsLocalRingHom f
[PROOFSTEP]
constructor
[GOAL]
case tfae_4_to_1.map_nonunit
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝³ : CommSemiring R
inst✝² : LocalRing R
inst✝¹ : CommSemiring S
inst✝ : LocalRing S
f : R →+* S
tfae_1_to_2 : IsLocalRingHom f → ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S)
tfae_2_to_4 :
  ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S) → maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_3_iff_4 : Ideal.map f (maximalIdeal R) ≤ maximalIdeal S ↔ maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
h : maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
⊢ ∀ (a : R), IsUnit (↑f a) → IsUnit a
[PROOFSTEP]
exact fun x => not_imp_not.1 (@h x)
[GOAL]
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝³ : CommSemiring R
inst✝² : LocalRing R
inst✝¹ : CommSemiring S
inst✝ : LocalRing S
f : R →+* S
tfae_1_to_2 : IsLocalRingHom f → ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S)
tfae_2_to_4 :
  ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S) → maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_3_iff_4 : Ideal.map f (maximalIdeal R) ≤ maximalIdeal S ↔ maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_4_to_1 : maximalIdeal R ≤ Ideal.comap f (maximalIdeal S) → IsLocalRingHom f
⊢ List.TFAE
    [IsLocalRingHom f, ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S),
      Ideal.map f (maximalIdeal R) ≤ maximalIdeal S, maximalIdeal R ≤ Ideal.comap f (maximalIdeal S),
      Ideal.comap f (maximalIdeal S) = maximalIdeal R]
[PROOFSTEP]
tfae_have 1 → 5
[GOAL]
case tfae_1_to_5
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝³ : CommSemiring R
inst✝² : LocalRing R
inst✝¹ : CommSemiring S
inst✝ : LocalRing S
f : R →+* S
tfae_1_to_2 : IsLocalRingHom f → ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S)
tfae_2_to_4 :
  ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S) → maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_3_iff_4 : Ideal.map f (maximalIdeal R) ≤ maximalIdeal S ↔ maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_4_to_1 : maximalIdeal R ≤ Ideal.comap f (maximalIdeal S) → IsLocalRingHom f
⊢ IsLocalRingHom f → Ideal.comap f (maximalIdeal S) = maximalIdeal R
[PROOFSTEP]
intro
[GOAL]
case tfae_1_to_5
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝³ : CommSemiring R
inst✝² : LocalRing R
inst✝¹ : CommSemiring S
inst✝ : LocalRing S
f : R →+* S
tfae_1_to_2 : IsLocalRingHom f → ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S)
tfae_2_to_4 :
  ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S) → maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_3_iff_4 : Ideal.map f (maximalIdeal R) ≤ maximalIdeal S ↔ maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_4_to_1 : maximalIdeal R ≤ Ideal.comap f (maximalIdeal S) → IsLocalRingHom f
✝ : IsLocalRingHom f
⊢ Ideal.comap f (maximalIdeal S) = maximalIdeal R
[PROOFSTEP]
ext
[GOAL]
case tfae_1_to_5.h
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝³ : CommSemiring R
inst✝² : LocalRing R
inst✝¹ : CommSemiring S
inst✝ : LocalRing S
f : R →+* S
tfae_1_to_2 : IsLocalRingHom f → ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S)
tfae_2_to_4 :
  ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S) → maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_3_iff_4 : Ideal.map f (maximalIdeal R) ≤ maximalIdeal S ↔ maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_4_to_1 : maximalIdeal R ≤ Ideal.comap f (maximalIdeal S) → IsLocalRingHom f
✝ : IsLocalRingHom f
x✝ : R
⊢ x✝ ∈ Ideal.comap f (maximalIdeal S) ↔ x✝ ∈ maximalIdeal R
[PROOFSTEP]
exact not_iff_not.2 (isUnit_map_iff f _)
[GOAL]
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝³ : CommSemiring R
inst✝² : LocalRing R
inst✝¹ : CommSemiring S
inst✝ : LocalRing S
f : R →+* S
tfae_1_to_2 : IsLocalRingHom f → ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S)
tfae_2_to_4 :
  ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S) → maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_3_iff_4 : Ideal.map f (maximalIdeal R) ≤ maximalIdeal S ↔ maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_4_to_1 : maximalIdeal R ≤ Ideal.comap f (maximalIdeal S) → IsLocalRingHom f
tfae_1_to_5 : IsLocalRingHom f → Ideal.comap f (maximalIdeal S) = maximalIdeal R
⊢ List.TFAE
    [IsLocalRingHom f, ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S),
      Ideal.map f (maximalIdeal R) ≤ maximalIdeal S, maximalIdeal R ≤ Ideal.comap f (maximalIdeal S),
      Ideal.comap f (maximalIdeal S) = maximalIdeal R]
[PROOFSTEP]
tfae_have 5 → 4
[GOAL]
case tfae_5_to_4
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝³ : CommSemiring R
inst✝² : LocalRing R
inst✝¹ : CommSemiring S
inst✝ : LocalRing S
f : R →+* S
tfae_1_to_2 : IsLocalRingHom f → ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S)
tfae_2_to_4 :
  ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S) → maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_3_iff_4 : Ideal.map f (maximalIdeal R) ≤ maximalIdeal S ↔ maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_4_to_1 : maximalIdeal R ≤ Ideal.comap f (maximalIdeal S) → IsLocalRingHom f
tfae_1_to_5 : IsLocalRingHom f → Ideal.comap f (maximalIdeal S) = maximalIdeal R
⊢ Ideal.comap f (maximalIdeal S) = maximalIdeal R → maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
[PROOFSTEP]
exact fun h => le_of_eq h.symm
[GOAL]
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝³ : CommSemiring R
inst✝² : LocalRing R
inst✝¹ : CommSemiring S
inst✝ : LocalRing S
f : R →+* S
tfae_1_to_2 : IsLocalRingHom f → ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S)
tfae_2_to_4 :
  ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S) → maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_3_iff_4 : Ideal.map f (maximalIdeal R) ≤ maximalIdeal S ↔ maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_4_to_1 : maximalIdeal R ≤ Ideal.comap f (maximalIdeal S) → IsLocalRingHom f
tfae_1_to_5 : IsLocalRingHom f → Ideal.comap f (maximalIdeal S) = maximalIdeal R
tfae_5_to_4 : Ideal.comap f (maximalIdeal S) = maximalIdeal R → maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
⊢ List.TFAE
    [IsLocalRingHom f, ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S),
      Ideal.map f (maximalIdeal R) ≤ maximalIdeal S, maximalIdeal R ≤ Ideal.comap f (maximalIdeal S),
      Ideal.comap f (maximalIdeal S) = maximalIdeal R]
[PROOFSTEP]
tfae_finish
[GOAL]
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝⁴ : CommSemiring R
inst✝³ : LocalRing R
inst✝² : CommSemiring S
inst✝¹ : Nontrivial S
f : R →+* S
inst✝ : IsLocalRingHom f
hf : Function.Surjective ↑f
⊢ ∀ (a b : S), IsUnit (a + b) → IsUnit a ∨ IsUnit b
[PROOFSTEP]
intro a b hab
[GOAL]
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝⁴ : CommSemiring R
inst✝³ : LocalRing R
inst✝² : CommSemiring S
inst✝¹ : Nontrivial S
f : R →+* S
inst✝ : IsLocalRingHom f
hf : Function.Surjective ↑f
a b : S
hab : IsUnit (a + b)
⊢ IsUnit a ∨ IsUnit b
[PROOFSTEP]
obtain ⟨a, rfl⟩ := hf a
[GOAL]
case intro
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝⁴ : CommSemiring R
inst✝³ : LocalRing R
inst✝² : CommSemiring S
inst✝¹ : Nontrivial S
f : R →+* S
inst✝ : IsLocalRingHom f
hf : Function.Surjective ↑f
b : S
a : R
hab : IsUnit (↑f a + b)
⊢ IsUnit (↑f a) ∨ IsUnit b
[PROOFSTEP]
obtain ⟨b, rfl⟩ := hf b
[GOAL]
case intro.intro
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝⁴ : CommSemiring R
inst✝³ : LocalRing R
inst✝² : CommSemiring S
inst✝¹ : Nontrivial S
f : R →+* S
inst✝ : IsLocalRingHom f
hf : Function.Surjective ↑f
a b : R
hab : IsUnit (↑f a + ↑f b)
⊢ IsUnit (↑f a) ∨ IsUnit (↑f b)
[PROOFSTEP]
rw [← map_add] at hab 
[GOAL]
case intro.intro
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝⁴ : CommSemiring R
inst✝³ : LocalRing R
inst✝² : CommSemiring S
inst✝¹ : Nontrivial S
f : R →+* S
inst✝ : IsLocalRingHom f
hf : Function.Surjective ↑f
a b : R
hab : IsUnit (↑f (a + b))
⊢ IsUnit (↑f a) ∨ IsUnit (↑f b)
[PROOFSTEP]
exact (isUnit_or_isUnit_of_isUnit_add <| IsLocalRingHom.map_nonunit _ hab).imp f.isUnit_map f.isUnit_map
[GOAL]
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
h : IsLocalRingHom f
⊢ Function.Surjective ↑(Units.map ↑f)
[PROOFSTEP]
intro a
[GOAL]
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
h : IsLocalRingHom f
a : Sˣ
⊢ ∃ a_1, ↑(Units.map ↑f) a_1 = a
[PROOFSTEP]
obtain ⟨b, hb⟩ := hf (a : S)
[GOAL]
case intro
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
h : IsLocalRingHom f
a : Sˣ
b : R
hb : ↑f b = ↑a
⊢ ∃ a_1, ↑(Units.map ↑f) a_1 = a
[PROOFSTEP]
use(isUnit_of_map_unit f b (by rw [hb]; exact Units.isUnit _)).unit
[GOAL]
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
h : IsLocalRingHom f
a : Sˣ
b : R
hb : ↑f b = ↑a
⊢ IsUnit (↑f b)
[PROOFSTEP]
rw [hb]
[GOAL]
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
h : IsLocalRingHom f
a : Sˣ
b : R
hb : ↑f b = ↑a
⊢ IsUnit ↑a
[PROOFSTEP]
exact Units.isUnit _
[GOAL]
case h
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
h : IsLocalRingHom f
a : Sˣ
b : R
hb : ↑f b = ↑a
⊢ ↑(Units.map ↑f) (IsUnit.unit (_ : IsUnit b)) = a
[PROOFSTEP]
ext
[GOAL]
case h.a
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
h : IsLocalRingHom f
a : Sˣ
b : R
hb : ↑f b = ↑a
⊢ ↑(↑(Units.map ↑f) (IsUnit.unit (_ : IsUnit b))) = ↑a
[PROOFSTEP]
exact hb
[GOAL]
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
f : R →+* S
inst✝ : IsLocalRingHom f
a : R
ha : a ∈ maximalIdeal R
⊢ ↑(RingHom.comp (Ideal.Quotient.mk (maximalIdeal S)) f) a = 0
[PROOFSTEP]
erw [Ideal.Quotient.eq_zero_iff_mem]
[GOAL]
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
f : R →+* S
inst✝ : IsLocalRingHom f
a : R
ha : a ∈ maximalIdeal R
⊢ ↑f a ∈ maximalIdeal S
[PROOFSTEP]
exact map_nonunit f a ha
[GOAL]
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
f : R ≃+* S
x : ResidueField R
⊢ ↑(map ↑(RingEquiv.symm f)) (↑(map ↑f) x) = x
[PROOFSTEP]
simp only [map_map, RingEquiv.symm_comp, map_id, RingHom.id_apply]
[GOAL]
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
f : R ≃+* S
x : ResidueField S
⊢ ↑(map ↑f) (↑(map ↑(RingEquiv.symm f)) x) = x
[PROOFSTEP]
simp only [map_map, RingEquiv.comp_symm, map_id, RingHom.id_apply]
[GOAL]
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)
[PROOFSTEP]
constructor
[GOAL]
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
[PROOFSTEP]
intro a ha
[GOAL]
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
[PROOFSTEP]
by_contra h
[GOAL]
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
[PROOFSTEP]
erw [Ideal.Quotient.eq_zero_iff_mem.mpr ((LocalRing.mem_maximalIdeal _).mpr h)] at ha 
[GOAL]
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
[PROOFSTEP]
exact ha.ne_zero rfl
[GOAL]
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝ : Field K
a : K
h : a = 0
⊢ IsUnit (1 - a)
[PROOFSTEP]
rw [h, sub_zero]
[GOAL]
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝ : Field K
a : K
h : a = 0
⊢ IsUnit 1
[PROOFSTEP]
exact isUnit_one
