toUnder — Mathlib

English

Two arrows f,g: mkUnder R A ⟶ B are equal iff their right components agree on every a ∈ A.

Русский

Две стрелки f,g: mkUnder R A ⟶ B равны тогда и только тогда, когда их правые компоненты совпадают на каждом a ∈ A.

LaTeX

$$$\forall a:\!A,\ f.right(a)=g.right(a) \Rightarrow f=g$$$

Lean4

/-- Make a morphism in `Under R` from an algebra map. -/
def toUnder {A B : Type u} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) :
    CommRingCat.mkUnder R A ⟶ CommRingCat.mkUnder R B :=
  Under.homMk (CommRingCat.ofHom f.toRingHom) <| by
    ext a
    exact f.commutes' a

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