Theorems · Definition · category theory

CategoryTheory.PreGaloisCategory.PointedGaloisObject.Hom.val

{C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    [inst_1 : CategoryTheory.GaloisCategory C] →
      {F : CategoryTheory.Functor C FintypeCat} →
        {A B : CategoryTheory.PreGaloisCategory.PointedGaloisObject F} → A.Hom B → (A.obj ⟶ B.obj)

The underlying homomorphism of C.

Defined in

Mathlib.CategoryTheory.Galois.Prorepresentability

Cited by

11 results in Mathlib

Foundations

Depth 14 from the axioms · uses propext

Assumes

CategoryTheory.CategoryCategoryTheory.GaloisCategory