Theorems · Theorem · category theory

CategoryTheory.PreGaloisCategory.autGaloisSystem_map_surjective

∀ {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⦄ (f : A ⟶ B),
  Function.Surjective
    ⇑(CategoryTheory.ConcreteCategory.hom ((CategoryTheory.PreGaloisCategory.autGaloisSystem F).map f))

Defined in

Mathlib.CategoryTheory.Galois.Prorepresentability

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.GaloisCategory