R : Type u
S : Type v
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | IsMaximal J} ∧ map C j = J
⊢ jacobson ⊥ ≤ J
R : Type u
S : Type v
inst✝ : CommRing R
⊢ jacobson ⊥ ≤ sInf (map C '' {J | IsMaximal J})
refine' le_sInf fun J => exists_imp.2 fun j hj => _
R : Type u
S : Type v
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | IsMaximal J} ∧ map C j = J
this : IsMaximal j
⊢ jacobson ⊥ ≤ J
R : Type u
S : Type v
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | IsMaximal J} ∧ map C j = J
⊢ jacobson ⊥ ≤ J
haveI : j.IsMaximal := hj.1
R : Type u
S : Type v
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | IsMaximal J} ∧ map C j = J
this : IsMaximal j
⊢ jacobson J = J
R : Type u
S : Type v
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | IsMaximal J} ∧ map C j = J
this : IsMaximal j
⊢ jacobson ⊥ ≤ J
refine' Trans.trans (jacobson_mono bot_le) (le_of_eq _ : J.jacobson ≤ J)
R : Type u
S : Type v
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | IsMaximal J} ∧ map C j = J
this : IsMaximal j
⊢ jacobson ⊥ = ⊥
R : Type u
S : Type v
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | IsMaximal J} ∧ map C j = J
this : IsMaximal j
⊢ jacobson J = J
suffices t : (⊥ : Ideal (Polynomial (R ⧸ j))).jacobson = ⊥ by
  rw [← hj.2, jacobson_eq_iff_jacobson_quotient_eq_bot]
  replace t := congr_arg (map (polynomialQuotientEquivQuotientPolynomial j).toRingHom) t
  rwa [map_jacobson_of_bijective _, map_bot] at t
  exact RingEquiv.bijective (polynomialQuotientEquivQuotientPolynomial j)
R : Type u
S : Type v
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | IsMaximal J} ∧ map C j = J
this : IsMaximal j
f : (R ⧸ j)[X]
hf : f ∈ jacobson ⊥
⊢ f ∈ ⊥
R : Type u
S : Type v
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | IsMaximal J} ∧ map C j = J
this : IsMaximal j
⊢ jacobson ⊥ = ⊥
refine' eq_bot_iff.2 fun f hf => _
R : Type u
S : Type v
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | IsMaximal J} ∧ map C j = J
this : IsMaximal j
f : (R ⧸ j)[X]
hf : f ∈ jacobson ⊥
r1 : X ≠ 0
⊢ f ∈ ⊥
R : Type u
S : Type v
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | IsMaximal J} ∧ map C j = J
this : IsMaximal j
f : (R ⧸ j)[X]
hf : f ∈ jacobson ⊥
⊢ f ∈ ⊥
have r1 : (X : (R ⧸ j)[X]) ≠ 0 := fun hX => by
  replace hX := congr_arg (fun f => coeff f 1) hX
  simp only [coeff_X_one, coeff_zero] at hX
  exact zero_ne_one hX.symm
R : Type u
S : Type v
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | IsMaximal J} ∧ map C j = J
this : IsMaximal j
f : (R ⧸ j)[X]
hf : f ∈ jacobson ⊥
r1 : X ≠ 0
r2 : f * X + 1 = ↑C (coeff (f * X + 1) 0)
⊢ f ∈ ⊥
R : Type u
S : Type v
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | IsMaximal J} ∧ map C j = J
this : IsMaximal j
f : (R ⧸ j)[X]
hf : f ∈ jacobson ⊥
r1 : X ≠ 0
⊢ f ∈ ⊥
have r2 := eq_C_of_degree_eq_zero (degree_eq_zero_of_isUnit ((mem_jacobson_bot.1 hf) X))
R : Type u
S : Type v
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | IsMaximal J} ∧ map C j = J
this : IsMaximal j
f : (R ⧸ j)[X]
hf : f ∈ jacobson ⊥
r1 : X ≠ 0
r2 : f * X + 1 = ↑C 1
⊢ f ∈ ⊥
R : Type u
S : Type v
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | IsMaximal J} ∧ map C j = J
this : IsMaximal j
f : (R ⧸ j)[X]
hf : f ∈ jacobson ⊥
r1 : X ≠ 0
r2 : f * X + 1 = ↑C (coeff (f * X + 1) 0)
⊢ f ∈ ⊥
simp only [coeff_add, mul_coeff_zero, coeff_X_zero, mul_zero, coeff_one_zero, zero_add] at r2
R : Type u
S : Type v
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | IsMaximal J} ∧ map C j = J
this : IsMaximal j
f : (R ⧸ j)[X]
hf : f ∈ jacobson ⊥
r1 : X ≠ 0
r2 : f * X = 0
⊢ f ∈ ⊥
R : Type u
S : Type v
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | IsMaximal J} ∧ map C j = J
this : IsMaximal j
f : (R ⧸ j)[X]
hf : f ∈ jacobson ⊥
r1 : X ≠ 0
r2 : f * X + 1 = ↑C 1
⊢ f ∈ ⊥
erw [add_left_eq_self] at r2
no goals
R : Type u
S : Type v
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | IsMaximal J} ∧ map C j = J
this : IsMaximal j
f : (R ⧸ j)[X]
hf : f ∈ jacobson ⊥
r1 : X ≠ 0
r2 : f * X = 0
⊢ f ∈ ⊥
simpa using (mul_eq_zero.mp r2).resolve_right r1
R : Type u
S : Type v
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | IsMaximal J} ∧ map C j = J
this : IsMaximal j
t : jacobson ⊥ = ⊥
⊢ jacobson ⊥ = ⊥
R : Type u
S : Type v
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | IsMaximal J} ∧ map C j = J
this : IsMaximal j
t : jacobson ⊥ = ⊥
⊢ jacobson J = J
rw [← hj.2, jacobson_eq_iff_jacobson_quotient_eq_bot]
R : Type u
S : Type v
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | IsMaximal J} ∧ map C j = J
this : IsMaximal j
t :
  map (RingEquiv.toRingHom (polynomialQuotientEquivQuotientPolynomial j)) (jacobson ⊥) =
    map (RingEquiv.toRingHom (polynomialQuotientEquivQuotientPolynomial j)) ⊥
⊢ jacobson ⊥ = ⊥
R : Type u
S : Type v
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | IsMaximal J} ∧ map C j = J
this : IsMaximal j
t : jacobson ⊥ = ⊥
⊢ jacobson ⊥ = ⊥
replace t := congr_arg (map (polynomialQuotientEquivQuotientPolynomial j).toRingHom) t
R : Type u
S : Type v
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | IsMaximal J} ∧ map C j = J
this : IsMaximal j
t :
  map (RingEquiv.toRingHom (polynomialQuotientEquivQuotientPolynomial j)) (jacobson ⊥) =
    map (RingEquiv.toRingHom (polynomialQuotientEquivQuotientPolynomial j)) ⊥
⊢ Function.Bijective ↑(RingEquiv.toRingHom (polynomialQuotientEquivQuotientPolynomial j))
R : Type u
S : Type v
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | IsMaximal J} ∧ map C j = J
this : IsMaximal j
t :
  map (RingEquiv.toRingHom (polynomialQuotientEquivQuotientPolynomial j)) (jacobson ⊥) =
    map (RingEquiv.toRingHom (polynomialQuotientEquivQuotientPolynomial j)) ⊥
⊢ jacobson ⊥ = ⊥
rwa [map_jacobson_of_bijective _, map_bot] at t
no goals
R : Type u
S : Type v
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | IsMaximal J} ∧ map C j = J
this : IsMaximal j
t :
  map (RingEquiv.toRingHom (polynomialQuotientEquivQuotientPolynomial j)) (jacobson ⊥) =
    map (RingEquiv.toRingHom (polynomialQuotientEquivQuotientPolynomial j)) ⊥
⊢ Function.Bijective ↑(RingEquiv.toRingHom (polynomialQuotientEquivQuotientPolynomial j))
exact RingEquiv.bijective (polynomialQuotientEquivQuotientPolynomial j)
R : Type u
S : Type v
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | IsMaximal J} ∧ map C j = J
this : IsMaximal j
f : (R ⧸ j)[X]
hf : f ∈ jacobson ⊥
hX : (fun f => coeff f 1) X = (fun f => coeff f 1) 0
⊢ False
R : Type u
S : Type v
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | IsMaximal J} ∧ map C j = J
this : IsMaximal j
f : (R ⧸ j)[X]
hf : f ∈ jacobson ⊥
hX : X = 0
⊢ False
replace hX := congr_arg (fun f => coeff f 1) hX
R : Type u
S : Type v
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | IsMaximal J} ∧ map C j = J
this : IsMaximal j
f : (R ⧸ j)[X]
hf : f ∈ jacobson ⊥
hX : 1 = 0
⊢ False
R : Type u
S : Type v
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | IsMaximal J} ∧ map C j = J
this : IsMaximal j
f : (R ⧸ j)[X]
hf : f ∈ jacobson ⊥
hX : (fun f => coeff f 1) X = (fun f => coeff f 1) 0
⊢ False
simp only [coeff_X_one, coeff_zero] at hX
no goals
R : Type u
S : Type v
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | IsMaximal J} ∧ map C j = J
this : IsMaximal j
f : (R ⧸ j)[X]
hf : f ∈ jacobson ⊥
hX : 1 = 0
⊢ False
exact zero_ne_one hX.symm