Arithmetic.lean
Nyll.EtaleFundamentalGroups.GeometricFiber.Arithmetic
0 declarations indexed from sourceView source ↗
Module documentation
Arithmetic fundamental-group maps, descent, and exactness.
Imports12
- Nyll.EtaleFundamentalGroups.GeometricFiber.ArithmeticSurjective
- Nyll.EtaleFundamentalGroups.GeometricFiber.AlgebraicClosureTower
- Nyll.EtaleFundamentalGroups.GeometricFiber.ArithmeticComposite
- Nyll.EtaleFundamentalGroups.GeometricFiber.ArithmeticConnected
- Nyll.EtaleFundamentalGroups.GeometricFiber.ArithmeticSections
- Nyll.EtaleFundamentalGroups.GeometricFiber.ArithmeticSectionFactorization
- Nyll.EtaleFundamentalGroups.GeometricFiber.ArithmeticNormal
- Nyll.EtaleFundamentalGroups.GeometricFiber.ArithmeticExact
- Nyll.EtaleFundamentalGroups.GeometricFiber.ArithmeticMap
- Nyll.EtaleFundamentalGroups.GeometricFiber.ArithmeticExactSequence
- Nyll.EtaleFundamentalGroups.GeometricFiber.ArithmeticAlgebraicClosure
- Nyll.EtaleFundamentalGroups.GeometricFiber.SeparableInjectivity
Imported by1
This module has no indexed declarations. Its imports and full source are available here.