Theorems · Theorem · category theory

CategoryTheory.PreGaloisCategory.evaluation_aut_injective_of_isConnected

∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat)
  [inst_1 : CategoryTheory.PreGaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] (A : C)
  [CategoryTheory.PreGaloisCategory.IsConnected A] (a : (F.obj A).obj),
  Function.Injective fun f => (CategoryTheory.ConcreteCategory.hom (F.map f.hom)) a

The evaluation map on automorphisms is injective for connected objects.

Defined in

Mathlib.CategoryTheory.Galois.Basic

Cited by

6 results in Mathlib

Foundations

Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.PreGaloisCategoryCategoryTheory.PreGaloisCategory.FiberFunctorCategoryTheory.PreGaloisCategory.IsConnected