hasForgetToRing — Mathlib

English

There is a forgetful functor from AlgCat R to RingCat, sending an algebra to its underlying ring and an algebra homomorphism to its underlying ring homomorphism.

Русский

Существует забывающий функтор из AlgCat R в RingCat, отправляющий алгебру в её основанное кольцо и алгебраический гомоморфизм — в соответствующий кольцевой гомоморфизм.

LaTeX

$$$\\text{forget}_2: \\mathrm{AlgCat}(R) \\to \\mathrm{RingCat}(R),\\ A \\mapsto \\mathrm{RingCat.of} A,\\ f \\mapsto \\mathrm{RingCat.ofHom}(f.hom)$$$

Lean4

instance hasForgetToRing : HasForget₂ (AlgCat.{v} R) RingCat.{v} where
  forget₂ :=
    { obj := fun A => RingCat.of A
      map := fun f => RingCat.ofHom f.hom.toRingHom }

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