BoundaryAndLocalFactors.lean
Nyll.EtaleFundamentalGroups.FiniteEtale.BoundaryAndLocalFactors
0 declarations indexed from sourceView source ↗
Module documentation
Boundary étaleness and local factors
Away, chosen-prime, Henselian, and local finite-étale results used in one-point inertia arguments.
Imports13
- Nyll.EtaleFundamentalGroups.FiniteEtale.Away.FinitePresentationExtension
- Nyll.EtaleFundamentalGroups.FiniteEtale.Away.GenericTensor.IntegralClosureBaseChange
- Nyll.EtaleFundamentalGroups.FiniteEtale.BaseChange.GenericTensor.NormalizationPrime
- Nyll.EtaleFundamentalGroups.FiniteEtale.Boundary.Complement
- Nyll.EtaleFundamentalGroups.FiniteEtale.ChosenPrime.Henselian.BoundaryAwayNoetherian
- Nyll.EtaleFundamentalGroups.FiniteEtale.ChosenPrime.PointedBase.BoundaryAway
- Nyll.EtaleFundamentalGroups.FiniteEtale.GenericFiber.ComponentDimensionTwo
- Nyll.SchemeTheory.FiniteEtale.Henselian.ChosenLocalizationEtale
- Nyll.SchemeTheory.FiniteEtale.Henselian.ResidueTrivialFiniteEtale
- Nyll.EtaleFundamentalGroups.FiniteEtale.HenselianAscent
- Nyll.SchemeTheory.FiniteEtale.Local.OfTargetLocalizations
- Nyll.EtaleFundamentalGroups.FiniteEtale.Local.OverDiscreteValuationRing
- Nyll.EtaleFundamentalGroups.FiniteEtale.Towers.IntegralTargetBoundaryAway
Imported by1
This module has no indexed declarations. Its imports and full source are available here.