Exact local principal-part dimensions at exhaustive places

The abstract DVR calculation in LocalPoleFiltration is instantiated at both the finite and infinity places of a finite separable extension of K(X). Thus every successive local pole layer has dimension exactly the degree of the corresponding exhaustive place.

@[instance_reducible]

noncomputable def BGS.HasseWeil.localQuotientConstantAlgebra (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra K L

The algebra structure from K to L used in the finite extension local pole quotient construction.

Equations

• BGS.HasseWeil.localQuotientConstantAlgebra K L = ((algebraMap (RatFunc K) L).comp (algebraMap K (RatFunc K))).toAlgebra

theorem BGS.HasseWeil.localQuotientConstantTower (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : IsScalarTower K (RatFunc K) L

@[instance_reducible]

noncomputable def BGS.HasseWeil.localQuotientPolynomialAlgebra (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra (Polynomial K) L

The algebra structure from K[X] to L used in the finite extension local pole quotient construction.

Equations

• BGS.HasseWeil.localQuotientPolynomialAlgebra K L = ((algebraMap (RatFunc K) L).comp (algebraMap (Polynomial K) (RatFunc K))).toAlgebra

theorem BGS.HasseWeil.localQuotientPolynomialTower (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : IsScalarTower (Polynomial K) (RatFunc K) L

@[instance_reducible]

noncomputable def BGS.HasseWeil.localQuotientFiniteClosureConstantAlgebra (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra K ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L)

The algebra structure from K to (RatFuncFiniteIntegralClosure K L) used in the finite extension local pole quotient construction.

Equations

• BGS.HasseWeil.localQuotientFiniteClosureConstantAlgebra K L = ((algebraMap (Polynomial K) ↥(BGS.CorvajaZannier.RatFuncFiniteIntegralClosure K L)).comp (algebraMap K (Polynomial K))).toAlgebra

theorem BGS.HasseWeil.localQuotientFiniteClosureConstantTower (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : IsScalarTower K (Polynomial K) ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L)

theorem BGS.HasseWeil.localQuotientFiniteClosureIsIntegral (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra.IsIntegral (Polynomial K) ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L)

theorem BGS.HasseWeil.localQuotientFiniteClosureModuleFinite (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Module.Finite (Polynomial K) ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L)

theorem BGS.HasseWeil.localQuotientPolynomialTorsionFreeTop (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Module.IsTorsionFree (Polynomial K) L

theorem BGS.HasseWeil.localQuotientFiniteClosureTorsionFree (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Module.IsTorsionFree (Polynomial K) ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L)

theorem BGS.HasseWeil.localQuotientFiniteClosureDedekind (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : IsDedekindDomain ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L)

theorem BGS.HasseWeil.localQuotientFiniteClosureFractionRing (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] : IsFractionRing (↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L)) L

theorem BGS.HasseWeil.finiteExtensionLocalPoleSpace_inl_step_finrank (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (q : CorvajaZannier.FiniteExtensionFinitePlace K L) (n : ℕ) : Module.finrank K (↥(finiteExtensionLocalPoleSpace K L (Sum.inl q) (n + 1)) ⧸ Submodule.comap (finiteExtensionLocalPoleSpace K L (Sum.inl q) (n + 1)).subtype (finiteExtensionLocalPoleSpace K L (Sum.inl q) n)) = CorvajaZannier.finiteExtensionPlaceDegree K L (Sum.inl q)

Every finite-place local principal-part layer has dimension exactly the degree of that place.

theorem BGS.HasseWeil.finiteExtensionLocalPoleSpace_inl_cumulative_finrank (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (q : CorvajaZannier.FiniteExtensionFinitePlace K L) (n : ℕ) : Module.finrank K (↥(finiteExtensionLocalPoleSpace K L (Sum.inl q) n) ⧸ Submodule.comap (finiteExtensionLocalPoleSpace K L (Sum.inl q) n).subtype (finiteExtensionLocalPoleSpace K L (Sum.inl q) 0)) = n * CorvajaZannier.finiteExtensionPlaceDegree K L (Sum.inl q)

The finite-place principal parts through order n have dimension n times the degree of the place.

@[instance_reducible]

noncomputable def BGS.HasseWeil.localQuotientInfinityConstantAlgebra (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] : Algebra K ↥(CorvajaZannier.RatFuncInfinityIntegers K)

The algebra structure from K to (RatFuncInfinityIntegers K) used in the finite extension local pole quotient construction.

Equations

• BGS.HasseWeil.localQuotientInfinityConstantAlgebra K = (BGS.CorvajaZannier.ratFuncInfinityConstantRingHom K).toAlgebra

@[instance_reducible]

noncomputable def BGS.HasseWeil.localQuotientInfinityClosureConstantAlgebra (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra K ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K L)

The algebra structure from K to (RatFuncInfinityIntegralClosure K L) used in the finite extension local pole quotient construction.

Equations

• One or more equations did not get rendered due to their size.

theorem BGS.HasseWeil.localQuotientInfinityClosureConstantTower (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : IsScalarTower K ↥(CorvajaZannier.RatFuncInfinityIntegers K) ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K L)

theorem BGS.HasseWeil.localQuotientInfinityClosureModuleFinite (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Module.Finite ↥(CorvajaZannier.RatFuncInfinityIntegers K) ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K L)

theorem BGS.HasseWeil.localQuotientInfinityClosureIsIntegral (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra.IsIntegral ↥(CorvajaZannier.RatFuncInfinityIntegers K) ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K L)

theorem BGS.HasseWeil.localQuotientInfinityBaseTorsionFreeTop (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Module.IsTorsionFree (↥(CorvajaZannier.RatFuncInfinityIntegers K)) L

theorem BGS.HasseWeil.localQuotientInfinityClosureTorsionFree (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Module.IsTorsionFree ↥(CorvajaZannier.RatFuncInfinityIntegers K) ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K L)

theorem BGS.HasseWeil.localQuotientInfinityClosureDedekind (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : IsDedekindDomain ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K L)

theorem BGS.HasseWeil.localQuotientInfinityClosureFractionRing (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] : IsFractionRing (↥(CorvajaZannier.RatFuncInfinityIntegralClosure K L)) L

theorem BGS.HasseWeil.localQuotientInfinityClosureConstantTowerToField (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : IsScalarTower K (↥(CorvajaZannier.RatFuncInfinityIntegralClosure K L)) L

theorem BGS.HasseWeil.finiteExtensionLocalPoleSpace_inr_step_finrank (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (P : ↑(CorvajaZannier.FiniteExtensionInfinityPlace K L)) (n : ℕ) : Module.finrank K (↥(finiteExtensionLocalPoleSpace K L (Sum.inr P) (n + 1)) ⧸ Submodule.comap (finiteExtensionLocalPoleSpace K L (Sum.inr P) (n + 1)).subtype (finiteExtensionLocalPoleSpace K L (Sum.inr P) n)) = CorvajaZannier.finiteExtensionPlaceDegree K L (Sum.inr P)

Every infinity-place local principal-part layer has dimension exactly the degree of that place.

theorem BGS.HasseWeil.finiteExtensionLocalPoleSpace_inr_cumulative_finrank (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (P : ↑(CorvajaZannier.FiniteExtensionInfinityPlace K L)) (n : ℕ) : Module.finrank K (↥(finiteExtensionLocalPoleSpace K L (Sum.inr P) n) ⧸ Submodule.comap (finiteExtensionLocalPoleSpace K L (Sum.inr P) n).subtype (finiteExtensionLocalPoleSpace K L (Sum.inr P) 0)) = n * CorvajaZannier.finiteExtensionPlaceDegree K L (Sum.inr P)

The infinity-place principal parts through order n have dimension n times the degree of the place.

theorem BGS.HasseWeil.finiteExtensionLocalPoleSpace_step_finrank (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (P : CorvajaZannier.FiniteExtensionPlace K L) (n : ℕ) : Module.finrank K (↥(finiteExtensionLocalPoleSpace K L P (n + 1)) ⧸ Submodule.comap (finiteExtensionLocalPoleSpace K L P (n + 1)).subtype (finiteExtensionLocalPoleSpace K L P n)) = CorvajaZannier.finiteExtensionPlaceDegree K L P

At every exhaustive place, each successive local pole layer has exact dimension equal to the place degree.

theorem BGS.HasseWeil.finiteExtensionLocalPoleSpace_cumulative_finrank (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (P : CorvajaZannier.FiniteExtensionPlace K L) (n : ℕ) : Module.finrank K (↥(finiteExtensionLocalPoleSpace K L P n) ⧸ Submodule.comap (finiteExtensionLocalPoleSpace K L P n).subtype (finiteExtensionLocalPoleSpace K L P 0)) = n * CorvajaZannier.finiteExtensionPlaceDegree K L P

At every exhaustive place, the principal parts through order n have dimension n times the place degree.