evaluation_aut_injective_of_isConnected

English

Let A be connected and a ∈ F.obj A. Then the map Aut(A) → F.obj A, sending f to F.map f.hom a, is injective.

Русский

Пусть A связный и a ∈ F.obj A. Тогда отображение Aut(A) → F.obj A, f ↦ F.map f.hom a, инъективно.

LaTeX

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

Lean4

/-- The evaluation map on automorphisms is injective for connected objects. -/
theorem evaluation_aut_injective_of_isConnected (A : C) [IsConnected A] (a : F.obj A) :
    Function.Injective (fun f : Aut A ↦ F.map (f.hom) a) :=
  by
  change Function.Injective ((fun f : A ⟶ A ↦ F.map f a) ∘ (fun f : Aut A ↦ f.hom))
  apply Function.Injective.comp
  · exact evaluation_injective_of_isConnected F A A a
  · exact @Aut.ext _ _ A

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