R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
h : RingHom.ker f ≤ I
⊢ map f (jacobson I) = jacobson (map f I)
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
⊢ RingHom.ker f ≤ I → map f (jacobson I) = jacobson (map f I)
intro h
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
h : RingHom.ker f ≤ I
⊢ map f (sInf {J | I ≤ J ∧ IsMaximal J}) = sInf {J | map f I ≤ J ∧ IsMaximal J}
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
h : RingHom.ker f ≤ I
⊢ map f (jacobson I) = jacobson (map f I)
unfold Ideal.jacobson
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
h : RingHom.ker f ≤ I
this : ∀ (J : Ideal R), J ∈ {J | I ≤ J ∧ IsMaximal J} → RingHom.ker f ≤ J
⊢ map f (sInf {J | I ≤ J ∧ IsMaximal J}) = sInf {J | map f I ≤ J ∧ IsMaximal J}
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
h : RingHom.ker f ≤ I
⊢ map f (sInf {J | I ≤ J ∧ IsMaximal J}) = sInf {J | map f I ≤ J ∧ IsMaximal J}
have : ∀ J ∈ { J : Ideal R | I ≤ J ∧ J.IsMaximal }, RingHom.ker f ≤ J :=
  fun J hJ => le_trans h hJ.left
case refine_1
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
h : RingHom.ker f ≤ I
this : ∀ (J : Ideal R), J ∈ {J | I ≤ J ∧ IsMaximal J} → RingHom.ker f ≤ J
⊢ sInf (map f '' {J | I ≤ J ∧ IsMaximal J}) ≤ sInf {J | map f I ≤ J ∧ IsMaximal J}

case refine_2
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
h : RingHom.ker f ≤ I
this : ∀ (J : Ideal R), J ∈ {J | I ≤ J ∧ IsMaximal J} → RingHom.ker f ≤ J
⊢ sInf {J | map f I ≤ J ∧ IsMaximal J} ≤ sInf (map f '' {J | I ≤ J ∧ IsMaximal J})
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
h : RingHom.ker f ≤ I
this : ∀ (J : Ideal R), J ∈ {J | I ≤ J ∧ IsMaximal J} → RingHom.ker f ≤ J
⊢ map f (sInf {J | I ≤ J ∧ IsMaximal J}) = sInf {J | map f I ≤ J ∧ IsMaximal J}
refine Trans.trans (map_sInf hf this) (le_antisymm ?_ ?_)
case refine_1
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
h : RingHom.ker f ≤ I
this : ∀ (J : Ideal R), J ∈ {J | I ≤ J ∧ IsMaximal J} → RingHom.ker f ≤ J
J : Ideal S
hJ : J ∈ {J | map f I ≤ J ∧ IsMaximal J}
⊢ IsMaximal (comap f J)
case refine_1
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
h : RingHom.ker f ≤ I
this : ∀ (J : Ideal R), J ∈ {J | I ≤ J ∧ IsMaximal J} → RingHom.ker f ≤ J
⊢ sInf (map f '' {J | I ≤ J ∧ IsMaximal J}) ≤ sInf {J | map f I ≤ J ∧ IsMaximal J}
refine'
  sInf_le_sInf fun J hJ =>
    ⟨comap f J, ⟨⟨le_comap_of_map_le hJ.1, _⟩, map_comap_of_surjective f hf J⟩⟩
case refine_1
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
h : RingHom.ker f ≤ I
this✝ : ∀ (J : Ideal R), J ∈ {J | I ≤ J ∧ IsMaximal J} → RingHom.ker f ≤ J
J : Ideal S
hJ : J ∈ {J | map f I ≤ J ∧ IsMaximal J}
this : IsMaximal J
⊢ IsMaximal (comap f J)
case refine_1
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
h : RingHom.ker f ≤ I
this : ∀ (J : Ideal R), J ∈ {J | I ≤ J ∧ IsMaximal J} → RingHom.ker f ≤ J
J : Ideal S
hJ : J ∈ {J | map f I ≤ J ∧ IsMaximal J}
⊢ IsMaximal (comap f J)
haveI : J.IsMaximal := hJ.right
no goals
case refine_1
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
h : RingHom.ker f ≤ I
this✝ : ∀ (J : Ideal R), J ∈ {J | I ≤ J ∧ IsMaximal J} → RingHom.ker f ≤ J
J : Ideal S
hJ : J ∈ {J | map f I ≤ J ∧ IsMaximal J}
this : IsMaximal J
⊢ IsMaximal (comap f J)
exact comap_isMaximal_of_surjective f hf
case refine_2
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
h : RingHom.ker f ≤ I
this : ∀ (J : Ideal R), J ∈ {J | I ≤ J ∧ IsMaximal J} → RingHom.ker f ≤ J
j : Ideal S
hj : j ∈ map f '' {J | I ≤ J ∧ IsMaximal J}
J : Ideal R
hJ : J ∈ {J | I ≤ J ∧ IsMaximal J} ∧ map f J = j
⊢ j ∈ insert ⊤ {J | map f I ≤ J ∧ IsMaximal J}
case refine_2
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
h : RingHom.ker f ≤ I
this : ∀ (J : Ideal R), J ∈ {J | I ≤ J ∧ IsMaximal J} → RingHom.ker f ≤ J
⊢ sInf {J | map f I ≤ J ∧ IsMaximal J} ≤ sInf (map f '' {J | I ≤ J ∧ IsMaximal J})
refine' sInf_le_sInf_of_subset_insert_top fun j hj => hj.recOn fun J hJ => _
case refine_2
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
h : RingHom.ker f ≤ I
this : ∀ (J : Ideal R), J ∈ {J | I ≤ J ∧ IsMaximal J} → RingHom.ker f ≤ J
j : Ideal S
hj : j ∈ map f '' {J | I ≤ J ∧ IsMaximal J}
J : Ideal R
hJ : J ∈ {J | I ≤ J ∧ IsMaximal J} ∧ map f J = j
⊢ map f J ∈ insert ⊤ {J | map f I ≤ J ∧ IsMaximal J}
case refine_2
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
h : RingHom.ker f ≤ I
this : ∀ (J : Ideal R), J ∈ {J | I ≤ J ∧ IsMaximal J} → RingHom.ker f ≤ J
j : Ideal S
hj : j ∈ map f '' {J | I ≤ J ∧ IsMaximal J}
J : Ideal R
hJ : J ∈ {J | I ≤ J ∧ IsMaximal J} ∧ map f J = j
⊢ j ∈ insert ⊤ {J | map f I ≤ J ∧ IsMaximal J}
rw [← hJ.2]
case refine_2.inl
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
h : RingHom.ker f ≤ I
this : ∀ (J : Ideal R), J ∈ {J | I ≤ J ∧ IsMaximal J} → RingHom.ker f ≤ J
j : Ideal S
hj : j ∈ map f '' {J | I ≤ J ∧ IsMaximal J}
J : Ideal R
hJ : J ∈ {J | I ≤ J ∧ IsMaximal J} ∧ map f J = j
htop : map f J = ⊤
⊢ map f J ∈ insert ⊤ {J | map f I ≤ J ∧ IsMaximal J}

case refine_2.inr
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
h : RingHom.ker f ≤ I
this : ∀ (J : Ideal R), J ∈ {J | I ≤ J ∧ IsMaximal J} → RingHom.ker f ≤ J
j : Ideal S
hj : j ∈ map f '' {J | I ≤ J ∧ IsMaximal J}
J : Ideal R
hJ : J ∈ {J | I ≤ J ∧ IsMaximal J} ∧ map f J = j
hmax : IsMaximal (map f J)
⊢ map f J ∈ insert ⊤ {J | map f I ≤ J ∧ IsMaximal J}
case refine_2
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
h : RingHom.ker f ≤ I
this : ∀ (J : Ideal R), J ∈ {J | I ≤ J ∧ IsMaximal J} → RingHom.ker f ≤ J
j : Ideal S
hj : j ∈ map f '' {J | I ≤ J ∧ IsMaximal J}
J : Ideal R
hJ : J ∈ {J | I ≤ J ∧ IsMaximal J} ∧ map f J = j
⊢ map f J ∈ insert ⊤ {J | map f I ≤ J ∧ IsMaximal J}
cases' map_eq_top_or_isMaximal_of_surjective f hf hJ.left.right with htop hmax
no goals
case refine_2.inl
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
h : RingHom.ker f ≤ I
this : ∀ (J : Ideal R), J ∈ {J | I ≤ J ∧ IsMaximal J} → RingHom.ker f ≤ J
j : Ideal S
hj : j ∈ map f '' {J | I ≤ J ∧ IsMaximal J}
J : Ideal R
hJ : J ∈ {J | I ≤ J ∧ IsMaximal J} ∧ map f J = j
htop : map f J = ⊤
⊢ map f J ∈ insert ⊤ {J | map f I ≤ J ∧ IsMaximal J}
exact htop.symm ▸ Set.mem_insert ⊤ _
no goals
case refine_2.inr
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
h : RingHom.ker f ≤ I
this : ∀ (J : Ideal R), J ∈ {J | I ≤ J ∧ IsMaximal J} → RingHom.ker f ≤ J
j : Ideal S
hj : j ∈ map f '' {J | I ≤ J ∧ IsMaximal J}
J : Ideal R
hJ : J ∈ {J | I ≤ J ∧ IsMaximal J} ∧ map f J = j
hmax : IsMaximal (map f J)
⊢ map f J ∈ insert ⊤ {J | map f I ≤ J ∧ IsMaximal J}
exact Set.mem_insert_of_mem ⊤ ⟨map_mono hJ.1.1, hmax⟩