ModuleResidueNumericalInvariants.lean
Nyll.AnabelianGeometry.WeightFiltration.ResidueNumericalInvariants
2 declarations indexed from sourceView source ↗ Module documentation
Recovering numerical invariants from the actual residue filtration
For an exponent greater than one, the kernel determines the genus and the image determines the size of a nonempty boundary. These are explicit numerical formulas. Recognition of the filtration from arithmetic group data is a separate theorem and is not an assumption hidden in this file.
Declarations
AnabelianGeometry.WeightFiltration.genus_eq_log_card_finiteResidue_ker
DocumentationThe actual residue kernel determines the genus.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory AlgebraicCurve NeronModelInfra
namespace AnabelianGeometry.WeightFiltration
variable {K F : Type} [Field K] [IsAlgClosed K] [CharZero K]
[Field F] [Algebra K F] [IsCurveOver K F]
(M : CurveModel K F)
(ε : SchemeHomOver (𝟙 (Spec (.of K))) M.toBase)
(n : ℕ+)
{X : Scheme} [IsIntegral X] [CompactSpace X]
(j : X ⟶ M.C) [IsOpenImmersion j] (hj : DenseRange j)
(hn : IsUnit ((n : ℕ) : K))
{Ω : Type} [Field Ω] [IsSepClosed Ω] (xi : Spec (.of Ω) ⟶ X)
include ε
AnabelianGeometry.WeightFiltration.boundaryCard_eq_log_card_finiteResidue_range
DocumentationFor nonempty boundary, its cardinality is one plus the logarithm of the actual residue-image cardinality. The empty boundary is excluded explicitly.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory AlgebraicCurve NeronModelInfra
namespace AnabelianGeometry.WeightFiltration
variable {K F : Type} [Field K] [IsAlgClosed K] [CharZero K]
[Field F] [Algebra K F] [IsCurveOver K F]
(M : CurveModel K F)
(ε : SchemeHomOver (𝟙 (Spec (.of K))) M.toBase)
(n : ℕ+)
{X : Scheme} [IsIntegral X] [CompactSpace X]
(j : X ⟶ M.C) [IsOpenImmersion j] (hj : DenseRange j)
(hn : IsUnit ((n : ℕ) : K))
{Ω : Type} [Field Ω] [IsSepClosed Ω] (xi : Spec (.of Ω) ⟶ X)
include ε
variable [Fintype (M.openBoundaryPlaces j)]
omit [CharZero K] in