All.lean
Nyll.EtaleFundamentalGroups.GaloisCategories.All
0 declarations indexed from sourceView source ↗
Module documentation
Galois categories and finite continuous actions
This facade collects reconstruction, fiber-functor comparison, functoriality, and exact-sequence results for Galois categories.
Canonical aggregate for EtaleFundamentalGroups.GaloisCategories.
Imports29
- Nyll.EtaleFundamentalGroups.GaloisCategories.AutomorphismProfiniteCompletion
- Nyll.EtaleFundamentalGroups.GaloisCategories.ConnectedActions
- Nyll.EtaleFundamentalGroups.GaloisCategories.ContinuousHomComparison
- Nyll.EtaleFundamentalGroups.GaloisCategories.DiscreteCharacters
- Nyll.EtaleFundamentalGroups.GaloisCategories.ExactSequence
- Nyll.EtaleFundamentalGroups.GaloisCategories.FiberFunctorComparison
- Nyll.EtaleFundamentalGroups.GaloisCategories.FiberFunctorExactness
- Nyll.EtaleFundamentalGroups.GaloisCategories.FiberFunctorUniqueness
- Nyll.EtaleFundamentalGroups.GaloisCategories.FiberIso
- Nyll.EtaleFundamentalGroups.GaloisCategories.FunctorFromHom
- Nyll.EtaleFundamentalGroups.GaloisCategories.Functoriality
- Nyll.EtaleFundamentalGroups.GaloisCategories.GaloisObjectQuotient
- Nyll.EtaleFundamentalGroups.GaloisCategories.Injectivity
- Nyll.EtaleFundamentalGroups.GaloisCategories.NormalImage
- Nyll.EtaleFundamentalGroups.GaloisCategories.PointedOver
- Nyll.EtaleFundamentalGroups.GaloisCategories.PointedOverTransport
- Nyll.EtaleFundamentalGroups.GaloisCategories.PointedDeckTransport
- Nyll.EtaleFundamentalGroups.GaloisCategories.RelativeDeckTransitivity
- Nyll.EtaleFundamentalGroups.GaloisCategories.Surjectivity
- Nyll.EtaleFundamentalGroups.GaloisCategories.TrivialComposite
- Nyll.EtaleFundamentalGroups.GaloisCategories.TrivialQuotient
- Nyll.EtaleFundamentalGroups.GaloisCategories.SectionFactorizationEpi
- Nyll.EtaleFundamentalGroups.GaloisCategories.FiberIsoKernel
- Nyll.EtaleFundamentalGroups.GaloisCategories.GaloisObjectFixedFiber
- Nyll.EtaleFundamentalGroups.GaloisCategories.AutomorphismDescent
- Nyll.EtaleFundamentalGroups.GaloisCategories.AutomorphismInverseLimit
- Nyll.EtaleFundamentalGroups.GaloisCategories.ConnectedSectionDescent
- Nyll.EtaleFundamentalGroups.GaloisCategories.AutFunctorComparison
- Nyll.EtaleFundamentalGroups.GaloisCategories.PointStabilizerMorphism
Imported by1
This module has no indexed declarations. Its imports and full source are available here.