Local traces and the different #
Relate different multiplicities to the trace-dual lattice and clear the finitely many bad valuation bounds by a base multiplier.
theorem
FractionalIdeal.le_iff_count_ge
{R : Type u_1}
[CommRing R]
[IsDedekindDomain R]
{K : Type u_2}
[Field K]
[Algebra R K]
[IsFractionRing R K]
{I J : FractionalIdeal (nonZeroDivisors R) K}
(hI : I ≠ 0)
(hJ : J ≠ 0)
:
theorem
FractionalIdeal.count_coeIdeal_eq_multiplicity
{R : Type u_1}
[CommRing R]
[IsDedekindDomain R]
{K : Type u_2}
[Field K]
[Algebra R K]
[IsFractionRing R K]
(I : Ideal R)
(hI : I ≠ ⊥)
(v : IsDedekindDomain.HeightOneSpectrum R)
:
theorem
FractionalIdeal.mem_iff_count_ge
{R : Type u_1}
[CommRing R]
[IsDedekindDomain R]
{K : Type u_2}
[Field K]
[Algebra R K]
[IsFractionRing R K]
{I : FractionalIdeal (nonZeroDivisors R) K}
(hI : I ≠ 0)
{x : K}
(hx : x ≠ 0)
:
x ∈ I ↔ ∀ (v : IsDedekindDomain.HeightOneSpectrum R), count K v I ≤ count K v ((spanSingleton (nonZeroDivisors R)) x)
theorem
HeightOneSpectrum.algebraMap_mem_pow_of_mem_under_pow
(A : Type u_3)
{B : Type u_5}
[CommRing A]
[CommRing B]
[Algebra A B]
[IsDedekindDomain B]
[Algebra.IsIntegral A B]
[IsDomain A]
(q : IsDedekindDomain.HeightOneSpectrum B)
(c : A)
(n : ℕ)
(hc : c ∈ (IsDedekindDomain.HeightOneSpectrum.under A q).asIdeal ^ n)
:
theorem
HeightOneSpectrum.natCast_le_count_spanSingleton_algebraMap_of_mem_under_pow
(A : Type u_3)
{L : Type u}
{B : Type u_5}
[CommRing A]
[CommRing B]
[Field L]
[Algebra B L]
[Algebra A B]
[Algebra A L]
[IsScalarTower A B L]
[IsFractionRing B L]
[IsDedekindDomain B]
[Module.IsTorsionFree A B]
[Algebra.IsIntegral A B]
[IsDomain A]
(q : IsDedekindDomain.HeightOneSpectrum B)
(c : A)
(n : ℕ)
(hc0 : c ≠ 0)
(hc : c ∈ (IsDedekindDomain.HeightOneSpectrum.under A q).asIdeal ^ n)
:
↑n ≤ FractionalIdeal.count L q ((FractionalIdeal.spanSingleton (nonZeroDivisors B)) ((algebraMap A L) c))
theorem
BGS.HasseWeil.count_dual_one_eq_neg_different_multiplicity
(A : Type u_3)
(K₀ : Type u_4)
{L : Type u}
{B : Type u_5}
[CommRing A]
[Field K₀]
[CommRing B]
[Field L]
[Algebra A K₀]
[Algebra B L]
[Algebra A B]
[Algebra K₀ L]
[Algebra A L]
[IsScalarTower A K₀ L]
[IsScalarTower A B L]
[IsFractionRing A K₀]
[FiniteDimensional K₀ L]
[Algebra.IsSeparable K₀ L]
[IsIntegralClosure B A L]
[IsFractionRing B L]
[IsIntegrallyClosed A]
[IsDedekindDomain B]
[Module.IsTorsionFree A B]
[IsDomain A]
(q : IsDedekindDomain.HeightOneSpectrum B)
:
FractionalIdeal.count L q (FractionalIdeal.dual A K₀ 1) = -↑(multiplicity q.asIdeal (differentIdeal A B))
theorem
BGS.HasseWeil.mem_dual_one_iff_different_multiplicity_le_count
(A : Type u_3)
(K₀ : Type u_4)
{L : Type u}
{B : Type u_5}
[CommRing A]
[Field K₀]
[CommRing B]
[Field L]
[Algebra A K₀]
[Algebra B L]
[Algebra A B]
[Algebra K₀ L]
[Algebra A L]
[IsScalarTower A K₀ L]
[IsScalarTower A B L]
[IsFractionRing A K₀]
[FiniteDimensional K₀ L]
[Algebra.IsSeparable K₀ L]
[IsIntegralClosure B A L]
[IsFractionRing B L]
[IsIntegrallyClosed A]
[IsDedekindDomain B]
[Module.IsTorsionFree A B]
[IsDomain A]
{x : L}
(hx : x ≠ 0)
:
x ∈ FractionalIdeal.dual A K₀ 1 ↔ ∀ (q : IsDedekindDomain.HeightOneSpectrum B),
-↑(multiplicity q.asIdeal (differentIdeal A B)) ≤ FractionalIdeal.count L q ((FractionalIdeal.spanSingleton (nonZeroDivisors B)) x)
theorem
BGS.HasseWeil.trace_mem_algebraMap_range_of_different_multiplicity_le_count
(A : Type u_3)
(K₀ : Type u_4)
{L : Type u}
{B : Type u_5}
[CommRing A]
[Field K₀]
[CommRing B]
[Field L]
[Algebra A K₀]
[Algebra B L]
[Algebra A B]
[Algebra K₀ L]
[Algebra A L]
[IsScalarTower A K₀ L]
[IsScalarTower A B L]
[IsFractionRing A K₀]
[FiniteDimensional K₀ L]
[Algebra.IsSeparable K₀ L]
[IsIntegralClosure B A L]
[IsFractionRing B L]
[IsIntegrallyClosed A]
[IsDedekindDomain B]
[Module.IsTorsionFree A B]
[IsDomain A]
{z : L}
(hz : z ≠ 0)
(hcount :
∀ (q : IsDedekindDomain.HeightOneSpectrum B),
-↑(multiplicity q.asIdeal (differentIdeal A B)) ≤ FractionalIdeal.count L q ((FractionalIdeal.spanSingleton (nonZeroDivisors B)) z))
:
theorem
BGS.HasseWeil.finite_badDifferentCount_set
(A : Type u_3)
{L : Type u}
{B : Type u_5}
[CommRing A]
[CommRing B]
[Field L]
[Algebra B L]
[Algebra A B]
[IsFractionRing B L]
[IsDedekindDomain B]
[Module.IsTorsionFree A B]
[IsDomain A]
(hdiff : differentIdeal A B ≠ ⊥)
(y : L)
:
{q : IsDedekindDomain.HeightOneSpectrum B | ¬-↑(multiplicity q.asIdeal (differentIdeal A B)) ≤ FractionalIdeal.count L q ((FractionalIdeal.spanSingleton (nonZeroDivisors B)) y)}.Finite
theorem
BGS.HasseWeil.exists_base_multiplier_clearing_different_counts
(A : Type u_3)
{L : Type u}
{B : Type u_5}
[CommRing A]
[CommRing B]
[Field L]
[Algebra B L]
[Algebra A B]
[Algebra A L]
[IsScalarTower A B L]
[IsFractionRing B L]
[IsDedekindDomain B]
[Module.IsTorsionFree A B]
[Algebra.IsIntegral A B]
[IsDedekindDomain A]
(hdiff : differentIdeal A B ≠ ⊥)
(p : IsDedekindDomain.HeightOneSpectrum A)
{y : L}
(hy : y ≠ 0)
(hlocal :
∀ (q : IsDedekindDomain.HeightOneSpectrum B),
IsDedekindDomain.HeightOneSpectrum.under A q = p →
-↑(multiplicity q.asIdeal (differentIdeal A B)) ≤ FractionalIdeal.count L q ((FractionalIdeal.spanSingleton (nonZeroDivisors B)) y))
:
∃ c ∉ p.asIdeal,
∀ (q : IsDedekindDomain.HeightOneSpectrum B),
-↑(multiplicity q.asIdeal (differentIdeal A B)) ≤ FractionalIdeal.count L q ((FractionalIdeal.spanSingleton (nonZeroDivisors B)) ((algebraMap A L) c * y))
theorem
BGS.HasseWeil.valuation_trace_le_one_of_different_count_bounds_over
(A : Type u_3)
(K₀ : Type u_4)
{L : Type u}
{B : Type u_5}
[CommRing A]
[Field K₀]
[CommRing B]
[Field L]
[Algebra A K₀]
[Algebra B L]
[Algebra A B]
[Algebra K₀ L]
[Algebra A L]
[IsScalarTower A K₀ L]
[IsScalarTower A B L]
[IsFractionRing A K₀]
[FiniteDimensional K₀ L]
[Algebra.IsSeparable K₀ L]
[IsIntegralClosure B A L]
[IsFractionRing B L]
[IsDedekindDomain B]
[Module.IsTorsionFree A B]
[Algebra.IsIntegral A B]
[IsDedekindDomain A]
(p : IsDedekindDomain.HeightOneSpectrum A)
{y : L}
(hy : y ≠ 0)
(hlocal :
∀ (q : IsDedekindDomain.HeightOneSpectrum B),
IsDedekindDomain.HeightOneSpectrum.under A q = p →
-↑(multiplicity q.asIdeal (differentIdeal A B)) ≤ FractionalIdeal.count L q ((FractionalIdeal.spanSingleton (nonZeroDivisors B)) y))
: