algEquivQuotAlgEquiv — Mathlib

English

If two R-algebras are R-equivalent and their quotients by a relation are defined, then their quotients are also R-equivalent.

Русский

Если два R-алгебра эквивалентны над R и их частные отношения определены, то и их частные отношения эквивалентны над R.

LaTeX

$$$\\text{algEquivQuotAlgEquiv }(f, rel)$$$

Lean4

/-- If two `R`-algebras are `R`-equivalent and their quotients by a relation `rel` are defined,
then their quotients are also `R`-equivalent.

(Special case of the third isomorphism theorem.) -/
def algEquivQuotAlgEquiv {R : Type u} [CommSemiring R] {A B : Type v} [Semiring A] [Semiring B] [Algebra R A]
    [Algebra R B] (f : A ≃ₐ[R] B) (rel : A → A → Prop) : RingQuot rel ≃ₐ[R] RingQuot (rel on f.symm) :=
  AlgEquiv.ofAlgHom
    (RingQuot.liftAlgHom R (s := rel)
      ⟨AlgHom.comp (RingQuot.mkAlgHom R (rel on f.symm)) f, fun x y h_rel ↦
        by
        apply RingQuot.mkAlgHom_rel
        simpa [Function.onFun]⟩)
    ((RingQuot.liftAlgHom R (s := rel on f.symm)
      ⟨AlgHom.comp (RingQuot.mkAlgHom R rel) f.symm, fun x y h ↦ by apply RingQuot.mkAlgHom_rel; simpa⟩))
    (by ext b; simp) (by ext a; simp)

Похожие утверждения