relative_isMultiplicative — Mathlib

English

If F is faithful, full and P is multiplicative, and P respects iso, then P.relative F is multiplicative as a morphism property.

Русский

Если F верен и полон, а P мультипликативно, и P уважает изоморфизмы, то P.relative F мультипликативно как свойство морфизмов.

LaTeX

$$$\text{IsMultiplicative}(P) \Rightarrow \text{IsMultiplicative}(P.relative F)$$$

Lean4

instance relative_isMultiplicative [F.Faithful] [F.Full] [P.IsMultiplicative] [P.RespectsIso] :
    IsMultiplicative (P.relative F) where
  id_mem X := relative.of_exists (fun Y g ↦ ⟨Y, g, 𝟙 Y, by simpa using IsPullback.of_id_snd, id_mem _ _⟩)

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