Module

PointStabilizerMorphism.lean

Nyll.EtaleFundamentalGroups.GaloisCategories.PointStabilizerMorphism

1 declaration indexed from sourceView source ↗

Module documentation

Realizing inclusion of actual point stabilizers

For connected objects, inclusion of the actual stabilizers of two fiber points gives a morphism taking the first point to the second. The map is constructed as an equivariant map and lifted by the full fiber-action functor. No equality between a proposed geometric morphism and subgroup inclusion is assumed. The fiber and category universes may differ.

Imports1

Mathlib.CategoryTheory.Galois.Full

Imported by2

theorem

exists_hom_of_pointStabilizer_le

L28 ↗

CategoryTheory.PreGaloisCategory.exists_hom_of_pointStabilizer_le

Documentation

Realize an inclusion of actual point stabilizers by a pointed morphism.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v w
open CategoryTheory
namespace CategoryTheory.PreGaloisCategory

Lean source · statement

theorem exists_hom_of_pointStabilizer_le
    {C : Type u} [Category.{v} C] [GaloisCategory C]
    (F : C ⥤ FintypeCat.{w}) [FiberFunctor F]
    (A B : C) [IsConnected A] (x : F.obj A) (y : F.obj B)
    (hxy : MulAction.stabilizer (Aut F) x ≤ MulAction.stabilizer (Aut F) y) :
    ∃ f : A ⟶ B, F.map f x = y

Module documentation

Realizing inclusion of actual point stabilizers

Declarations

exists_hom_of_pointStabilizer_le