ModuleComponentGenericInertiaCardinality.lean
Nyll.EtaleFundamentalGroups.Kummer.NormalCrossings.ComponentGenericInertiaCardinality
21 declarations indexed from sourceView source ↗ Module documentation
Inertia cardinality at a fixed boundary component
The branch prime attached to a component at any of its specializations has the component generic stalk as its prime localization. This identifies the ramification index seen in every specialized stalk with one fixed index at the component generic point.
Declarations
AlgebraicGeometry.Scheme.stalkSpecializationEquivLocalization
DocumentationThe canonical identification of a generization stalk with the corresponding prime localization.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory TopologicalSpace
namespace AlgebraicGeometry.Scheme
universe u
AlgebraicGeometry.Scheme.stalkSpecializationEquivLocalization_comp_stalkSpecializes
DocumentationThe canonical identification of a generization stalk with the corresponding prime localization extends the generization map.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory TopologicalSpace
namespace AlgebraicGeometry.Scheme
universe u
AlgebraicGeometry.Scheme.stalkSpecializes_isLocalization
DocumentationA generization map of scheme stalks is the localization at the prime represented by that generization.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory TopologicalSpace
namespace AlgebraicGeometry.Scheme
universe u
AlgebraicGeometry.Scheme.stalkFunctionFieldAlgebra_comp_stalkSpecializes
DocumentationThe maps from specialized and generization stalks to the function field of an integral scheme commute with the generization map.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory TopologicalSpace
namespace AlgebraicGeometry.Scheme
universe u
AlgebraicGeometry.Scheme.IdealSheafData.supportComplementFunctionFieldAlgebra_comp_stalkSpecializes
DocumentationThe maps from specialized and generization stalks to the function field of an ideal-sheaf complement commute with the generization map.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory TopologicalSpace
namespace AlgebraicGeometry.Scheme
universe u
AlgebraicGeometry.Scheme.IdealSheafData.supportComplementFunctionFieldAlgebra_comp_stalkSpecializationEquiv
DocumentationUnder the canonical prime-localization model, the map from a component generic stalk to the complement function field is unchanged.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory TopologicalSpace
namespace AlgebraicGeometry.Scheme
universe u
AlgebraicGeometry.Scheme.IdealSheafData.componentGenericNormalizationPrimeOver
DocumentationA normalization prime over the closed point of the fixed component generic stalk. This is selected once, independently of any later specialization of the component.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory TopologicalSpace
namespace AlgebraicGeometry.Scheme
universe u
AlgebraicGeometry.Scheme.IdealSheafData.componentGenericNormalizationPrime
DocumentationThe underlying fixed normalization prime at the component generic point.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory TopologicalSpace
namespace AlgebraicGeometry.Scheme
universe u
AlgebraicGeometry.Scheme.IdealSheafData.componentGenericNormalizationPrime_isPrime
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory TopologicalSpace
namespace AlgebraicGeometry.Scheme
universe u
AlgebraicGeometry.Scheme.IdealSheafData.componentGenericNormalizationPrime_liesOver
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory TopologicalSpace
namespace AlgebraicGeometry.Scheme
universe u
AlgebraicGeometry.Scheme.IdealSheafData.componentGenericNormalizationRamificationIndex
DocumentationThe fixed ramification index attached to a boundary component and a function-field extension.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory TopologicalSpace
namespace AlgebraicGeometry.Scheme
universe u
EtaleFundamentalGroups.Ideal.under_map_eq_map_under_of_compatible_ringEquiv
DocumentationCompatible equivalences carry the contraction of a target ideal to the corresponding base ideal.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory TopologicalSpace
namespace EtaleFundamentalGroups
universe uR uS uT uU
AlgebraicGeometry.Scheme.IdealSheafData.normalizationPrime_ramificationIdx_eq_componentGeneric
DocumentationA normalization prime above the branch of a fixed component in any specialized stalk has the fixed component-generic ramification index.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory TopologicalSpace
namespace AlgebraicGeometry.Scheme.IdealSheafData
open EtaleFundamentalGroups
universe u
variable {X : Scheme.{u}}
AlgebraicGeometry.Scheme.IdealSheafData.normalizationInertia_card_eq_componentGenericRamificationIndex
DocumentationAt a characteristic-zero component branch, the inertia cardinality in a specialized stalk is the fixed component-generic ramification index.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory TopologicalSpace
namespace AlgebraicGeometry.Scheme.IdealSheafData
open EtaleFundamentalGroups
universe u
variable {X : Scheme.{u}}
AlgebraicGeometry.Scheme.IdealSheafData.normalizationInertia_card_eq_componentGenericRamificationIndex_of_eq
DocumentationEquality-transport form of normalizationInertia_card_eq_componentGenericRamificationIndex, matching the ambient stalk returned by an etale chart whose image point is identified with the prescribed component specialization.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory TopologicalSpace
namespace AlgebraicGeometry.Scheme.IdealSheafData
open EtaleFundamentalGroups
universe u
variable {X : Scheme.{u}}
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory TopologicalSpace
namespace AlgebraicGeometry.Scheme.EffectiveCartierDivisor
open CategoryTheory.PreGaloisCategory EtaleFundamentalGroups
universe u
variable {X : Scheme.{u}}
AlgebraicGeometry.Scheme.EffectiveCartierDivisor.HasSurjectiveComponentsOverIntegers.forall_prime_componentGenericNormalizationRamificationIndex_coprime
DocumentationFor a fixed component and a fixed connected Galois cover, its one component-generic ramification index is prime to every rational prime. The specialized normalization prime used for each rational prime may vary, but the integer on the left does not.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory TopologicalSpace
namespace AlgebraicGeometry.Scheme.EffectiveCartierDivisor
open CategoryTheory.PreGaloisCategory EtaleFundamentalGroups
universe u
variable {X : Scheme.{u}}
local instance : IsDomain (ULift.{u} ℤ) :=
(ULift.ringEquiv : ULift.{u} ℤ ≃+* ℤ).toMulEquiv.isDomain ℤ
namespace HasSurjectiveComponentsOverIntegers
AlgebraicGeometry.Scheme.EffectiveCartierDivisor.HasSurjectiveComponentsOverIntegers.componentGenericNormalizationRamificationIndex_eq_one
DocumentationThe fixed component-generic ramification index is one. Indeed, the same natural number is prime to every rational prime by specializing the component in every positive residue characteristic.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory TopologicalSpace
namespace AlgebraicGeometry.Scheme.EffectiveCartierDivisor
open CategoryTheory.PreGaloisCategory EtaleFundamentalGroups
universe u
variable {X : Scheme.{u}}
local instance : IsDomain (ULift.{u} ℤ) :=
(ULift.ringEquiv : ULift.{u} ℤ ≃+* ℤ).toMulEquiv.isDomain ℤ
AlgebraicGeometry.Scheme.EffectiveCartierDivisor.IsHorizontalOver.componentGenericNormalizationInertia_card_eq_ramificationIndex
DocumentationThe inertia group at the fixed component-generic normalization prime has cardinality equal to the fixed component ramification index.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory TopologicalSpace
namespace AlgebraicGeometry.Scheme.EffectiveCartierDivisor
open CategoryTheory.PreGaloisCategory EtaleFundamentalGroups
universe u
variable {X : Scheme.{u}}
local instance : IsDomain (ULift.{u} ℤ) :=
(ULift.ringEquiv : ULift.{u} ℤ ≃+* ℤ).toMulEquiv.isDomain ℤ
AlgebraicGeometry.Scheme.EffectiveCartierDivisor.HasSurjectiveComponentsOverIntegers.forall_prime_componentGenericNormalizationInertia_card_coprime
DocumentationThe cardinality of one fixed divisorial inertia group is prime to every rational prime. Both the normalization prime and the inertia group are now independent of the residue characteristic used in the local argument.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory TopologicalSpace
namespace AlgebraicGeometry.Scheme.EffectiveCartierDivisor
open CategoryTheory.PreGaloisCategory EtaleFundamentalGroups
universe u
variable {X : Scheme.{u}}
local instance : IsDomain (ULift.{u} ℤ) :=
(ULift.ringEquiv : ULift.{u} ℤ ≃+* ℤ).toMulEquiv.isDomain ℤ
namespace HasSurjectiveComponentsOverIntegers
AlgebraicGeometry.Scheme.EffectiveCartierDivisor.HasSurjectiveComponentsOverIntegers.componentNormalizationInertia_eq_bot
DocumentationEvery normalization ideal inertia group above a specialization of the fixed boundary component is trivial. Its cardinality is the fixed component-generic ramification index, which is one by the all-prime specialization argument.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory TopologicalSpace
namespace AlgebraicGeometry.Scheme.EffectiveCartierDivisor
open CategoryTheory.PreGaloisCategory EtaleFundamentalGroups
universe u
variable {X : Scheme.{u}}
local instance : IsDomain (ULift.{u} ℤ) :=
(ULift.ringEquiv : ULift.{u} ℤ ≃+* ℤ).toMulEquiv.isDomain ℤ