autEmbedding — Mathlib

English

The embedding Aut(F) → ∏_X Aut(F.obj X) is a closed embedding.

Русский

Встраивание Aut(F) → ∏_X Aut(F.obj X) является замкнутым вложением.

LaTeX

$$IsClosedEmbedding(autEmbedding(F))$$

Lean4

/-- For a functor `F : C ⥤ FintypeCat`, the canonical embedding of `Aut F` into
the product over `Aut (F.obj X)` for all objects `X`. -/
def autEmbedding : Aut F →* ∀ X, Aut (F.obj X) :=
  MonoidHom.mk' (fun σ X ↦ σ.app X) (fun _ _ ↦ rfl)

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