R : Type u
S : Type v
F : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : RingHomClass F R S
f : F
I : Ideal R
hf : Function.Surjective ↑f
K : Ideal S
H : IsMaximal K
J : Ideal R
hJ : comap f K < J
⊢ J = ⊤
R : Type u
S : Type v
F : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : RingHomClass F R S
f : F
I : Ideal R
hf : Function.Surjective ↑f
K : Ideal S
H : IsMaximal K
⊢ IsMaximal (comap f K)
refine' ⟨⟨comap_ne_top _ H.1.1, fun J hJ => _⟩⟩
R : Type u
S : Type v
F : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : RingHomClass F R S
f : F
I : Ideal R
hf : Function.Surjective ↑f
K : Ideal S
H : IsMaximal K
J : Ideal R
hJ : comap f K < J
⊢ map f J = ⊤
R : Type u
S : Type v
F : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : RingHomClass F R S
f : F
I : Ideal R
hf : Function.Surjective ↑f
K : Ideal S
H : IsMaximal K
J : Ideal R
hJ : comap f K < J
⊢ J = ⊤
suffices map f J = ⊤ by
  have := congr_arg (comap f) this
  rw [comap_top, comap_map_of_surjective _ hf, eq_top_iff] at this
  rw [eq_top_iff]
  exact le_trans this (sup_le (le_of_eq rfl) (le_trans (comap_mono bot_le) (le_of_lt hJ)))
R : Type u
S : Type v
F : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : RingHomClass F R S
f : F
I : Ideal R
hf : Function.Surjective ↑f
K : Ideal S
H : IsMaximal K
J : Ideal R
hJ : comap f K < J
h : K = map f J
⊢ comap f (map f J) = J
R : Type u
S : Type v
F : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : RingHomClass F R S
f : F
I : Ideal R
hf : Function.Surjective ↑f
K : Ideal S
H : IsMaximal K
J : Ideal R
hJ : comap f K < J
⊢ map f J = ⊤
refine'
  H.1.2 (map f J)
    (lt_of_le_of_ne (le_map_of_comap_le_of_surjective _ hf (le_of_lt hJ)) fun h =>
      ne_of_lt hJ (_root_.trans (congr_arg (comap f) h) _))
R : Type u
S : Type v
F : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : RingHomClass F R S
f : F
I : Ideal R
hf : Function.Surjective ↑f
K : Ideal S
H : IsMaximal K
J : Ideal R
hJ : comap f K < J
h : K = map f J
⊢ comap f ⊥ ≤ J
R : Type u
S : Type v
F : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : RingHomClass F R S
f : F
I : Ideal R
hf : Function.Surjective ↑f
K : Ideal S
H : IsMaximal K
J : Ideal R
hJ : comap f K < J
h : K = map f J
⊢ comap f (map f J) = J
rw [comap_map_of_surjective _ hf, sup_eq_left]
no goals
R : Type u
S : Type v
F : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : RingHomClass F R S
f : F
I : Ideal R
hf : Function.Surjective ↑f
K : Ideal S
H : IsMaximal K
J : Ideal R
hJ : comap f K < J
h : K = map f J
⊢ comap f ⊥ ≤ J
exact le_trans (comap_mono bot_le) (le_of_lt hJ)
R : Type u
S : Type v
F : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : RingHomClass F R S
f : F
I : Ideal R
hf : Function.Surjective ↑f
K : Ideal S
H : IsMaximal K
J : Ideal R
hJ : comap f K < J
this✝ : map f J = ⊤
this : comap f (map f J) = comap f ⊤
⊢ J = ⊤
R : Type u
S : Type v
F : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : RingHomClass F R S
f : F
I : Ideal R
hf : Function.Surjective ↑f
K : Ideal S
H : IsMaximal K
J : Ideal R
hJ : comap f K < J
this : map f J = ⊤
⊢ J = ⊤
have := congr_arg (comap f) this
R : Type u
S : Type v
F : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : RingHomClass F R S
f : F
I : Ideal R
hf : Function.Surjective ↑f
K : Ideal S
H : IsMaximal K
J : Ideal R
hJ : comap f K < J
this✝ : map f J = ⊤
this : ⊤ ≤ J ⊔ comap f ⊥
⊢ J = ⊤
R : Type u
S : Type v
F : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : RingHomClass F R S
f : F
I : Ideal R
hf : Function.Surjective ↑f
K : Ideal S
H : IsMaximal K
J : Ideal R
hJ : comap f K < J
this✝ : map f J = ⊤
this : comap f (map f J) = comap f ⊤
⊢ J = ⊤
rw [comap_top, comap_map_of_surjective _ hf, eq_top_iff] at this
R : Type u
S : Type v
F : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : RingHomClass F R S
f : F
I : Ideal R
hf : Function.Surjective ↑f
K : Ideal S
H : IsMaximal K
J : Ideal R
hJ : comap f K < J
this✝ : map f J = ⊤
this : ⊤ ≤ J ⊔ comap f ⊥
⊢ ⊤ ≤ J
R : Type u
S : Type v
F : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : RingHomClass F R S
f : F
I : Ideal R
hf : Function.Surjective ↑f
K : Ideal S
H : IsMaximal K
J : Ideal R
hJ : comap f K < J
this✝ : map f J = ⊤
this : ⊤ ≤ J ⊔ comap f ⊥
⊢ J = ⊤
rw [eq_top_iff]
no goals
R : Type u
S : Type v
F : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : RingHomClass F R S
f : F
I : Ideal R
hf : Function.Surjective ↑f
K : Ideal S
H : IsMaximal K
J : Ideal R
hJ : comap f K < J
this✝ : map f J = ⊤
this : ⊤ ≤ J ⊔ comap f ⊥
⊢ ⊤ ≤ J
exact le_trans this (sup_le (le_of_eq rfl) (le_trans (comap_mono bot_le) (le_of_lt hJ)))