prodMap — Mathlib

English

ProdMap sends a pair of morphisms f1: A →A[R] B and f2: C →A[R] D to a morphism A × C →A[R] B × D by composing with fst and snd.

Русский

ProdMap переводит пару морфизмов в морфизм между произведениями через композицию с fst и snd.

LaTeX

$$prodMap {D} (f₁ : A →A[R] B) (f₂ : C →A[R] D) : A × C →A[R] B × D$$

Lean4

/-- `Prod.map` of two continuous algebra homomorphisms. -/
def prodMap {D : Type*} [Semiring D] [TopologicalSpace D] [Algebra R D] (f₁ : A →A[R] B) (f₂ : C →A[R] D) :
    A × C →A[R] B × D :=
  (f₁.comp (fst R A C)).prod (f₂.comp (snd R A C))

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