ModuleArithmeticCondition.lean
Nyll.EtaleFundamentalGroups.FiniteEtale.Boundary.ArithmeticCondition
3 declarations indexed from sourceView source ↗ Module documentation
Galois-cover arithmetic boundary conditions
This module owns the boundary conditions whose statements quantify over finite étale Galois covers.
Declarations
AlgebraicGeometry.Scheme.EffectiveCartierDivisor.HasGeometricallyIntegralGenericComponentsAfterGaloisCovers
DocumentationAfter every connected finite etale Galois cover, every irreducible component of the pulled-back divisor has geometrically integral generic fibre over the chosen integral base.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry
universe u
namespace Scheme
namespace EffectiveCartierDivisor
variable {X S : Scheme.{u}}
AlgebraicGeometry.Scheme.EffectiveCartierDivisor.SatisfiesResidueCharacteristicTwoBoundaryCondition
DocumentationAn arithmetic normal-crossings boundary condition at residue characteristic 2.
The ambient scheme is integral, normal and locally Noetherian. The conjunction explicitly contains reducedness and horizontality of the divisor, regularity along its support, a characteristic 2 normal-crossing point on every irreducible component, and geometric integrality of every generic boundary component after each connected finite etale Galois cover.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry
universe u
namespace Scheme
namespace EffectiveCartierDivisor
variable {X S : Scheme.{u}}
AlgebraicGeometry.Scheme.EffectiveCartierDivisor.SatisfiesResidueCharacteristicTwoBoundaryConditionOverIntegers
DocumentationThe residue-characteristic-two boundary condition over the integer base.
The structure morphism is not additional data: Spec ℤ is terminal in the category of schemes. ULift only places the integer base in the universe of X.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry
universe u
namespace Scheme
namespace EffectiveCartierDivisor
variable {X S : Scheme.{u}}