Theorems · Theorem · category theory

CategoryTheory.PreGaloisCategory.exists_set_ker_evaluation_subset_of_isOpen

∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat)
  [inst_1 : CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F]
  {H : Set (CategoryTheory.Aut F)},
  1 ∈ H →
    IsOpen H →
      ∃ I x,
        (∀ X ∈ I, CategoryTheory.PreGaloisCategory.IsConnected X) ∧
          ∀ (σ : CategoryTheory.Aut F), (∀ (X : ↑I), σ.hom.app ↑X = CategoryTheory.CategoryStruct.id (F.obj ↑X)) → σ ∈ H

If H is an open subset of Aut F such that 1 ∈ H, there exists a finite set I of connected objects of C such that every σ : Aut F that induces the identity on F.obj X for all X ∈ I is contained in H. In other words: The kernel of the evaluation map Aut F →* ∏ X : I ↦ Aut (F.obj X) is contained in H.

Defined in

Mathlib.CategoryTheory.Galois.Topology

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.GaloisCategoryCategoryTheory.PreGaloisCategory.FiberFunctor