All.lean
Nyll.EtaleFundamentalGroups.FiniteEtale.All
0 declarations indexed from sourceView source ↗
Module documentation
Finite étale covers and geometric fibers
This facade collects the geometric-fiber equivalence, covering-family criterion, and Galois-cover characterizations over the scheme-theoretic finite étale foundation.
Canonical aggregate for EtaleFundamentalGroups.FiniteEtale.
Imports71
- Nyll.EtaleFundamentalGroups.FiniteEtale.Away.All
- Nyll.EtaleFundamentalGroups.FiniteEtale.BaseChange.All
- Nyll.EtaleFundamentalGroups.FiniteEtale.Boundary.All
- Nyll.EtaleFundamentalGroups.FiniteEtale.BoundaryAndLocalFactors
- Nyll.EtaleFundamentalGroups.FiniteEtale.ChosenPrime.All
- Nyll.EtaleFundamentalGroups.FiniteEtale.Connected
- Nyll.EtaleFundamentalGroups.FiniteEtale.ConnectedComponents
- Nyll.EtaleFundamentalGroups.FiniteEtale.ConnectedComponentFaithful
- Nyll.EtaleFundamentalGroups.FiniteEtale.ConnectedReduction
- Nyll.EtaleFundamentalGroups.FiniteEtale.DensePullback
- Nyll.EtaleFundamentalGroups.FiniteEtale.DominantPreimmersionPullback
- Nyll.EtaleFundamentalGroups.FiniteEtale.DominantPreimmersionPullbackAbelian
- Nyll.EtaleFundamentalGroups.FiniteEtale.FiniteField.All
- Nyll.EtaleFundamentalGroups.FiniteEtale.FunctionField
- Nyll.EtaleFundamentalGroups.FiniteEtale.FunctionFieldNormalization
- Nyll.EtaleFundamentalGroups.FiniteEtale.GaloisDomination
- Nyll.EtaleFundamentalGroups.FiniteEtale.GenericFiber.All
- Nyll.EtaleFundamentalGroups.FiniteEtale.Henselian.All
- Nyll.EtaleFundamentalGroups.FiniteEtale.HenselianAscent
- Nyll.EtaleFundamentalGroups.FiniteEtale.HenselianPair
- Nyll.EtaleFundamentalGroups.FiniteEtale.Integers
- Nyll.EtaleFundamentalGroups.FiniteEtale.Integral
- Nyll.EtaleFundamentalGroups.FiniteEtale.InternalHom
- Nyll.EtaleFundamentalGroups.FiniteEtale.Local.All
- Nyll.EtaleFundamentalGroups.FiniteEtale.RegularSystem
- Nyll.EtaleFundamentalGroups.FiniteEtale.StalkFunctionFieldNormalization
- Nyll.EtaleFundamentalGroups.FiniteEtale.Thickening
- Nyll.EtaleFundamentalGroups.FiniteEtale.Towers.All
- Nyll.EtaleFundamentalGroups.FiniteEtale.TrivialCoverAlgebra
- Nyll.EtaleFundamentalGroups.FiniteEtale.TrivialBaseChangeAlgebra
- Nyll.EtaleFundamentalGroups.FiniteEtale.InverseLimitModels
- Nyll.EtaleFundamentalGroups.FiniteEtale.InverseLimitFractions
- Nyll.EtaleFundamentalGroups.FiniteEtale.InverseLimitStages
- Nyll.EtaleFundamentalGroups.FiniteEtale.InverseLimitFullness
- Nyll.EtaleFundamentalGroups.FiniteEtale.InverseLimitEventualFaithfulness
- Nyll.EtaleFundamentalGroups.FiniteEtale.InverseLimitFaithfulness
- Nyll.EtaleFundamentalGroups.FiniteEtale.InverseLimitDiagram
- Nyll.EtaleFundamentalGroups.FiniteEtale.InverseLimitFundamentalGroup
- Nyll.EtaleFundamentalGroups.FiniteEtale.InverseLimitFundamentalGroupSystem
- Nyll.EtaleFundamentalGroups.FiniteEtale.InverseLimitEventualHom
- Nyll.EtaleFundamentalGroups.FiniteEtale.InverseLimitStageCoherence
- Nyll.EtaleFundamentalGroups.FiniteEtale.InverseLimitEquivalence
- Nyll.EtaleFundamentalGroups.FiniteEtale.InverseLimitComparison
- Nyll.EtaleFundamentalGroups.FiniteEtale.LocalKernelBaseChange
- Nyll.EtaleFundamentalGroups.FiniteEtale.ProjectiveCokernelBaseChange
- Nyll.EtaleFundamentalGroups.FiniteEtale.StructureSheafSectionsEquiv
- Nyll.EtaleFundamentalGroups.FiniteEtale.ProperGeometricallyReducedSections
- Nyll.EtaleFundamentalGroups.FiniteEtale.ProperSectionsEtaleFieldDescent
- Nyll.EtaleFundamentalGroups.FiniteEtale.ClosedFiberEtaleDescent
- Nyll.EtaleFundamentalGroups.FiniteEtale.NoetherianLocalProperModel
- Nyll.EtaleFundamentalGroups.FiniteEtale.CechKernelBaseChangeSurjectivity
- Nyll.EtaleFundamentalGroups.FiniteEtale.ProperEtaleClosedFiberSections
- Nyll.EtaleFundamentalGroups.FiniteEtale.ProperLocalH0BaseChange
- Nyll.EtaleFundamentalGroups.FiniteEtale.ProperLocalSectionsBaseChange
- Nyll.EtaleFundamentalGroups.FiniteEtale.ProperLocalSectionAlgebra
- Nyll.EtaleFundamentalGroups.FiniteEtale.ProperLocalFiniteEtaleSections
- Nyll.EtaleFundamentalGroups.FiniteEtale.ProperLocalNormalization
- Nyll.EtaleFundamentalGroups.FiniteEtale.ProperIdempotentSectionLift
- Nyll.EtaleFundamentalGroups.FiniteEtale.ProperSplitClosedFiberSections
- Nyll.EtaleFundamentalGroups.FiniteEtale.ProperHenselianFullyFaithful
- Nyll.EtaleFundamentalGroups.FiniteEtale.AdicCoverTower
- Nyll.EtaleFundamentalGroups.FiniteEtale.UniversalHomeomorphism
- Nyll.EtaleFundamentalGroups.FiniteEtale.StalkObjectSpreading
- Nyll.EtaleFundamentalGroups.FiniteEtale.CompatibleStalkCoverSpreading
- Nyll.EtaleFundamentalGroups.FiniteEtale.ProperNoetherianSectionAlgebra
- Nyll.EtaleFundamentalGroups.FiniteEtale.ProperNoetherianNormalization
- Nyll.EtaleFundamentalGroups.FiniteEtale.ProperLocalScalarSections
- Nyll.EtaleFundamentalGroups.FiniteEtale.ProperNoetherianConnectedFibers
- Nyll.EtaleFundamentalGroups.FiniteEtale.ProperNoetherianModelSections
- Nyll.EtaleFundamentalGroups.FiniteEtale.ProperSectionAlgebra
- Nyll.EtaleFundamentalGroups.FiniteEtale.ProperNormalization
Imported by1
This module has no indexed declarations. Its imports and full source are available here.