All.lean
Nyll.Yamaguchi26SolvableCoverings.All
0 declarations indexed from sourceView source ↗
Module documentation
Extension of solvable coverings
Formalization of Naganori Yamaguchi's Extension of solvable coverings across horizontal divisors over the integers, using the numbering of arXiv v1. Includes the geometric, group-theoretic and representation-theoretic arguments.
Imports13
- Nyll.Yamaguchi26SolvableCoverings.Geometry.All
- Nyll.Yamaguchi26SolvableCoverings.GroupTheory.All
- Nyll.Yamaguchi26SolvableCoverings.Representations.All
- Nyll.Yamaguchi26SolvableCoverings.Theorem1Dot1BoundaryQuotient
- Nyll.Yamaguchi26SolvableCoverings.Theorem1Dot2InertiaControl
- Nyll.Yamaguchi26SolvableCoverings.Theorem1Dot3BoundaryInvariance
- Nyll.Yamaguchi26SolvableCoverings.Theorem1Dot4FundamentalGroupIntegers
- Nyll.Yamaguchi26SolvableCoverings.Theorem2Dot1AbelianInvariance
- Nyll.Yamaguchi26SolvableCoverings.Theorem2Dot2BoundaryCondition
- Nyll.Yamaguchi26SolvableCoverings.Theorem2Dot3SmoothBoundary
- Nyll.Yamaguchi26SolvableCoverings.Theorem2Dot4FiniteEtaleStability
- Nyll.Yamaguchi26SolvableCoverings.Theorem2Dot5PerfectKernel
- Nyll.Yamaguchi26SolvableCoverings.Theorem2Dot6ResidualExtension
Imported by1
This module has no indexed declarations. Its imports and full source are available here.