evaluation_injective_of_isConnected

English

Let A be connected and a ∈ F.obj A. Then the map f ↦ F.map f a from A ⟶ X to F.obj X is injective for every X.

Русский

Пусть A — связный объект и a ∈ F.obj A. Тогда отображение f : A ⟶ X, заданное f ↦ F.map f a, инъективно для любого X.

LaTeX

$$$\operatorname{Injective}\bigl(\lambda f: A \to X,\ F.map\ f\ a\bigr)$$$

Lean4

/-- The evaluation map is injective for connected objects. -/
theorem evaluation_injective_of_isConnected (A X : C) [IsConnected A] (a : F.obj A) :
    Function.Injective (fun (f : A ⟶ X) ↦ F.map f a) :=
  by
  intro f g (h : F.map f a = F.map g a)
  haveI : IsIso (equalizer.ι f g) :=
    by
    apply IsConnected.noTrivialComponent _ (equalizer.ι f g)
    exact not_initial_of_inhabited F ((fiberEqualizerEquiv F f g).symm ⟨a, h⟩)
  exact eq_of_epi_equalizer

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