English
If R is simple, then its opposite ring R^op is simple.
Русский
Если R простое, то противоположное кольцо R^op простое.
LaTeX
$$IsSimpleRing R ⇒ IsSimpleRing R^{op}.$$
Lean4
theorem exists_lift {B : Type u} [CommRing B] [_RB : Algebra R B] [FormallySmooth R A] (I : Ideal B)
(hI : IsNilpotent I) (g : A →ₐ[R] B ⧸ I) : ∃ f : A →ₐ[R] B, (Ideal.Quotient.mkₐ R I).comp f = g :=
by
revert g
change Function.Surjective (Ideal.Quotient.mkₐ R I).comp
revert _RB
apply Ideal.IsNilpotent.induction_on (S := B) I hI
· intro B _ I hI _; exact FormallySmooth.comp_surjective I hI
· intro B _ I J hIJ h₁ h₂ _ g
let this : ((B ⧸ I) ⧸ J.map (Ideal.Quotient.mk I)) ≃ₐ[R] B ⧸ J :=
{ (DoubleQuot.quotQuotEquivQuotSup I J).trans (Ideal.quotEquivOfEq (sup_eq_right.mpr hIJ)) with
commutes' := fun x => rfl }
obtain ⟨g', e⟩ := h₂ (this.symm.toAlgHom.comp g)
obtain ⟨g', rfl⟩ := h₁ g'
replace e := congr_arg this.toAlgHom.comp e
conv_rhs at e =>
rw [← AlgHom.comp_assoc, AlgEquiv.toAlgHom_eq_coe, AlgEquiv.toAlgHom_eq_coe, AlgEquiv.comp_symm, AlgHom.id_comp]
exact ⟨g', e⟩
