comap_comapₐ — Mathlib

English

If K is two-sided, then comap of an algebra homomorphism is two-sided.

Русский

Если K двусторонний, то comap расщепления алгебра-гомоморфизма тоже двусторонний.

LaTeX

$$$\text{If } K.IsTwoSided,\ (I.comap f K).IsTwoSided$$$

Lean4

theorem comap_comapₐ {R A B C : Type*} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B]
    [Semiring C] [Algebra R C] {I : Ideal C} (f : A →ₐ[R] B) (g : B →ₐ[R] C) :
    (I.comap g).comap f = I.comap (g.comp f) :=
  I.comap_comap f.toRingHom g.toRingHom

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