From cc5fa41481ab2ca6afd7332e44985e98d9fe98b9 Mon Sep 17 00:00:00 2001 From: Xavier Roblot Date: Thu, 31 Oct 2024 10:18:03 +0000 Subject: [PATCH] feat(NumberField/FundamentalCone): generalize the bijection to integral ideals (#18248) The norm-preserving bijection between the`integralPoint` in the fundamental cone and the integral ideals (times the torsion) is generalized to a bijection between the points of the fundamental cone lying in the image of an integral ideal `J` and the integral ideals divisible by `J` (times the torsion). This PR is part of the proof of the Analytic Class Number Formula. --- .../CanonicalEmbedding/FundamentalCone.lean | 370 +++++++++++------- 1 file changed, 232 insertions(+), 138 deletions(-) diff --git a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean index 419b0f6e623c0..c305edd79b369 100644 --- a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean +++ b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean @@ -5,6 +5,7 @@ Authors: Xavier Roblot -/ import Mathlib.RingTheory.Ideal.IsPrincipal import Mathlib.NumberTheory.NumberField.Units.DirichletTheorem +import Mathlib.RingTheory.ClassGroup /-! # Fundamental Cone @@ -23,17 +24,14 @@ by multiplication by a nonzero real number, see `smul_mem_of_mem`, that is also domain for the action of `(𝓞 K)ˣ` modulo torsion, see `exists_unit_smul_mem` and `torsion_unit_smul_mem_of_mem`. -* `NumberField.mixedEmbedding.fundamentalCone.integralPoint`: the subset of elements of the -fundamental cone that are images of algebraic integers of `K`. +* `NumberField.mixedEmbedding.fundamentalCone.idealSet`: for `J` an integral ideal, the intersection +between the fundamental cone and the `idealLattice` defined by the image of `J`. -* `NumberField.mixedEmbedding.fundamentalCone.integralPointEquiv`: the equivalence between -`fundamentalCone.integralPoint K` and the principal nonzero ideals of `𝓞 K` times the +* `NumberField.mixedEmbedding.fundamentalCone.idealSetEquivNorm`: for `J` an integral ideal and `n` +a natural integer, the equivalence between the elements of `idealSet K` of norm `n` and the +product of the set of nonzero principal ideals of `K` divisible by `J` of norm `n` and the torsion of `K`. -* `NumberField.mixedEmbedding.fundamentalCone.card_isPrincipal_norm_eq_mul_torsion`: the number of -principal nonzero ideals in `𝓞 K` of norm `n` multiplied by the order of the torsion of `K` is -equal to the number of `fundamentalCone.integralPoint K` of norm `n`. - ## Tags number field, canonical embedding, units, principal ideals @@ -247,159 +245,158 @@ theorem unit_smul_mem_iff_mem_torsion (hx : x ∈ fundamentalCone K) (u : (𝓞 exact hx.1 variable (K) in -/-- The set of images by `mixedEmbedding` of algebraic integers of `K` contained in the -fundamental cone. -/ -def integralPoint : Set (mixedSpace K) := +/-- The intersection between the fundamental cone and the `integerLattice`. -/ +def integerSet : Set (mixedSpace K) := fundamentalCone K ∩ mixedEmbedding.integerLattice K -theorem mem_integralPoint {a : mixedSpace K} : - a ∈ integralPoint K ↔ a ∈ fundamentalCone K ∧ ∃ x : 𝓞 K, mixedEmbedding K x = a := by - simp only [integralPoint, Set.mem_inter_iff, SetLike.mem_coe, LinearMap.mem_range, +theorem mem_integerSet {a : mixedSpace K} : + a ∈ integerSet K ↔ a ∈ fundamentalCone K ∧ ∃ x : 𝓞 K, mixedEmbedding K x = a := by + simp only [integerSet, Set.mem_inter_iff, SetLike.mem_coe, LinearMap.mem_range, AlgHom.toLinearMap_apply, RingHom.toIntAlgHom_coe, RingHom.coe_comp, Function.comp_apply] -/-- If `a` is an integral point, then there is a *unique* algebraic integer in `𝓞 K` such +/-- If `a` is in `integerSet`, then there is a *unique* algebraic integer in `𝓞 K` such that `mixedEmbedding K x = a`. -/ -theorem exists_unique_preimage_of_integralPoint {a : mixedSpace K} (ha : a ∈ integralPoint K) : +theorem exists_unique_preimage_of_mem_integerSet {a : mixedSpace K} (ha : a ∈ integerSet K) : ∃! x : 𝓞 K, mixedEmbedding K x = a := by - obtain ⟨_, ⟨x, rfl⟩⟩ := mem_integralPoint.mp ha + obtain ⟨_, ⟨x, rfl⟩⟩ := mem_integerSet.mp ha refine Function.Injective.existsUnique_of_mem_range ?_ (Set.mem_range_self x) exact (mixedEmbedding_injective K).comp RingOfIntegers.coe_injective -theorem integralPoint_ne_zero (a : integralPoint K) : (a : mixedSpace K) ≠ 0 := by +theorem ne_zero_of_mem_integerSet (a : integerSet K) : (a : mixedSpace K) ≠ 0 := by by_contra! exact a.prop.1.2 (this.symm ▸ mixedEmbedding.norm.map_zero') open scoped nonZeroDivisors -/-- For `a : fundamentalCone K`, the unique nonzero algebraic integer `x` such that its image by +/-- For `a : integerSet K`, the unique nonzero algebraic integer `x` such that its image by `mixedEmbedding` is equal to `a`. Note that we state the fact that `x ≠ 0` by saying that `x` is a nonzero divisors since we will use later on the isomorphism -`Ideal.associatesNonZeroDivisorsEquivIsPrincipal`, see `integralPointEquiv`. -/ -def preimageOfIntegralPoint (a : integralPoint K) : (𝓞 K)⁰ := - ⟨(mem_integralPoint.mp a.prop).2.choose, mem_nonZeroDivisors_of_ne_zero (by +`Ideal.associatesNonZeroDivisorsEquivIsPrincipal`, see `integerSetEquiv`. -/ +def preimageOfMemIntegerSet (a : integerSet K) : (𝓞 K)⁰ := + ⟨(mem_integerSet.mp a.prop).2.choose, mem_nonZeroDivisors_of_ne_zero (by simp_rw [ne_eq, ← RingOfIntegers.coe_injective.eq_iff, ← (mixedEmbedding_injective K).eq_iff, - map_zero, (mem_integralPoint.mp a.prop).2.choose_spec, integralPoint_ne_zero, + map_zero, (mem_integerSet.mp a.prop).2.choose_spec, ne_zero_of_mem_integerSet, not_false_eq_true])⟩ @[simp] -theorem mixedEmbedding_preimageOfIntegralPoint (a : integralPoint K) : - mixedEmbedding K (preimageOfIntegralPoint a : 𝓞 K) = (a : mixedSpace K) := by - rw [preimageOfIntegralPoint, (mem_integralPoint.mp a.prop).2.choose_spec] +theorem mixedEmbedding_preimageOfMemIntegerSet (a : integerSet K) : + mixedEmbedding K (preimageOfMemIntegerSet a : 𝓞 K) = (a : mixedSpace K) := by + rw [preimageOfMemIntegerSet, (mem_integerSet.mp a.prop).2.choose_spec] -theorem preimageOfIntegralPoint_mixedEmbedding {x : (𝓞 K)⁰} - (hx : mixedEmbedding K (x : 𝓞 K) ∈ integralPoint K) : - preimageOfIntegralPoint (⟨mixedEmbedding K (x : 𝓞 K), hx⟩) = x := by - simp_rw [Subtype.ext_iff, RingOfIntegers.ext_iff, ← (mixedEmbedding_injective K).eq_iff, - mixedEmbedding_preimageOfIntegralPoint] +theorem preimageOfMemIntegerSet_mixedEmbedding {x : (𝓞 K)} + (hx : mixedEmbedding K (x : 𝓞 K) ∈ integerSet K) : + preimageOfMemIntegerSet (⟨mixedEmbedding K (x : 𝓞 K), hx⟩) = x := by + simp_rw [RingOfIntegers.ext_iff, ← (mixedEmbedding_injective K).eq_iff, + mixedEmbedding_preimageOfMemIntegerSet] /-- If `x : mixedSpace K` is nonzero and the image of an algebraic integer, then there exists a -unit such that `u • x ∈ integralPoint K`. -/ -theorem exists_unitSMul_mem_integralPoint {x : mixedSpace K} (hx : x ≠ 0) +unit such that `u • x ∈ integerSet K`. -/ +theorem exists_unitSMul_mem_integerSet {x : mixedSpace K} (hx : x ≠ 0) (hx' : x ∈ mixedEmbedding K '' (Set.range (algebraMap (𝓞 K) K))) : - ∃ u : (𝓞 K)ˣ, u • x ∈ integralPoint K := by + ∃ u : (𝓞 K)ˣ, u • x ∈ integerSet K := by replace hx : mixedEmbedding.norm x ≠ 0 := (norm_eq_zero_iff' (Set.mem_range_of_mem_image (mixedEmbedding K) _ hx')).not.mpr hx obtain ⟨u, hu⟩ := exists_unit_smul_mem hx obtain ⟨_, ⟨x, rfl⟩, _, rfl⟩ := hx' - exact ⟨u, mem_integralPoint.mpr ⟨hu, u * x, by simp_rw [unitSMul_smul, ← map_mul]⟩⟩ + exact ⟨u, mem_integerSet.mpr ⟨hu, u * x, by simp_rw [unitSMul_smul, ← map_mul]⟩⟩ -/-- The set `integralPoint K` is stable under the action of the torsion. -/ -theorem torsion_unitSMul_mem_integralPoint {x : mixedSpace K} {ζ : (𝓞 K)ˣ} (hζ : ζ ∈ torsion K) - (hx : x ∈ integralPoint K) : ζ • x ∈ integralPoint K := by - obtain ⟨a, ⟨_, rfl⟩, rfl⟩ := (mem_integralPoint.mp hx).2 - refine mem_integralPoint.mpr ⟨torsion_smul_mem_of_mem hx.1 hζ, ⟨ζ * a, by simp⟩⟩ +/-- The set `integerSet K` is stable under the action of the torsion. -/ +theorem torsion_unitSMul_mem_integerSet {x : mixedSpace K} {ζ : (𝓞 K)ˣ} (hζ : ζ ∈ torsion K) + (hx : x ∈ integerSet K) : ζ • x ∈ integerSet K := by + obtain ⟨a, ⟨_, rfl⟩, rfl⟩ := (mem_integerSet.mp hx).2 + refine mem_integerSet.mpr ⟨torsion_smul_mem_of_mem hx.1 hζ, ⟨ζ * a, by simp⟩⟩ -/-- The action of `torsion K` on `integralPoint K`. -/ +/-- The action of `torsion K` on `integerSet K`. -/ @[simps] -instance integralPoint_torsionSMul: SMul (torsion K) (integralPoint K) where - smul := fun ⟨ζ, hζ⟩ ⟨x, hx⟩ ↦ ⟨ζ • x, torsion_unitSMul_mem_integralPoint hζ hx⟩ +instance integerSetTorsionSMul: SMul (torsion K) (integerSet K) where + smul := fun ⟨ζ, hζ⟩ ⟨x, hx⟩ ↦ ⟨ζ • x, torsion_unitSMul_mem_integerSet hζ hx⟩ -instance : MulAction (torsion K) (integralPoint K) where +instance : MulAction (torsion K) (integerSet K) where one_smul := fun _ ↦ by - rw [Subtype.mk_eq_mk, integralPoint_torsionSMul_smul_coe, OneMemClass.coe_one, one_smul] + rw [Subtype.mk_eq_mk, integerSetTorsionSMul_smul_coe, OneMemClass.coe_one, one_smul] mul_smul := fun _ _ _ ↦ by rw [Subtype.mk_eq_mk] - simp_rw [integralPoint_torsionSMul_smul_coe, Subgroup.coe_mul, mul_smul] + simp_rw [integerSetTorsionSMul_smul_coe, Subgroup.coe_mul, mul_smul] -/-- The `mixedEmbedding.norm` of `a : integralPoint K` as a natural number, see also +/-- The `mixedEmbedding.norm` of `a : integerSet K` as a natural number, see also `intNorm_coe`. -/ -def intNorm (a : integralPoint K) : ℕ := (Algebra.norm ℤ (preimageOfIntegralPoint a : 𝓞 K)).natAbs +def intNorm (a : integerSet K) : ℕ := (Algebra.norm ℤ (preimageOfMemIntegerSet a : 𝓞 K)).natAbs @[simp] -theorem intNorm_coe (a : integralPoint K) : +theorem intNorm_coe (a : integerSet K) : (intNorm a : ℝ) = mixedEmbedding.norm (a : mixedSpace K) := by rw [intNorm, Int.cast_natAbs, ← Rat.cast_intCast, Int.cast_abs, Algebra.coe_norm_int, - ← norm_eq_norm, mixedEmbedding_preimageOfIntegralPoint] + ← norm_eq_norm, mixedEmbedding_preimageOfMemIntegerSet] -/-- The norm `intNorm` lifts to a function on `integralPoint K` modulo `torsion K`. -/ +/-- The norm `intNorm` lifts to a function on `integerSet K` modulo `torsion K`. -/ def quotIntNorm : - Quotient (MulAction.orbitRel (torsion K) (integralPoint K)) → ℕ := + Quotient (MulAction.orbitRel (torsion K) (integerSet K)) → ℕ := Quotient.lift (fun x ↦ intNorm x) fun a b ⟨u, hu⟩ ↦ by - rw [← Nat.cast_inj (R := ℝ), intNorm_coe, intNorm_coe, ← hu, integralPoint_torsionSMul_smul_coe, + rw [← Nat.cast_inj (R := ℝ), intNorm_coe, intNorm_coe, ← hu, integerSetTorsionSMul_smul_coe, norm_unit_smul] @[simp] -theorem quotIntNorm_apply (a : integralPoint K) : quotIntNorm ⟦a⟧ = intNorm a := rfl +theorem quotIntNorm_apply (a : integerSet K) : quotIntNorm ⟦a⟧ = intNorm a := rfl variable (K) in -/-- The map that sends an element of `a : integralPoint K` to the associates class +/-- The map that sends an element of `a : integerSet K` to the associates class of its preimage in `(𝓞 K)⁰`. By quotienting by the kernel of the map, which is equal to the -subgroup of torsion, we get the equivalence `integralPointQuotEquivAssociates`. -/ -def integralPointToAssociates (a : integralPoint K) : Associates (𝓞 K)⁰ := - ⟦preimageOfIntegralPoint a⟧ +subgroup of torsion, we get the equivalence `integerSetQuotEquivAssociates`. -/ +def integerSetToAssociates (a : integerSet K) : Associates (𝓞 K)⁰ := + ⟦preimageOfMemIntegerSet a⟧ @[simp] -theorem integralPointToAssociates_apply (a : integralPoint K) : - integralPointToAssociates K a = ⟦preimageOfIntegralPoint a⟧ := rfl +theorem integerSetToAssociates_apply (a : integerSet K) : + integerSetToAssociates K a = ⟦preimageOfMemIntegerSet a⟧ := rfl variable (K) in -theorem integralPointToAssociates_surjective : - Function.Surjective (integralPointToAssociates K) := by +theorem integerSetToAssociates_surjective : + Function.Surjective (integerSetToAssociates K) := by rintro ⟨x⟩ - obtain ⟨u, hu⟩ : ∃ u : (𝓞 K)ˣ, u • mixedEmbedding K (x : 𝓞 K) ∈ integralPoint K := by - refine exists_unitSMul_mem_integralPoint ?_ ⟨(x : 𝓞 K), Set.mem_range_self _, rfl⟩ + obtain ⟨u, hu⟩ : ∃ u : (𝓞 K)ˣ, u • mixedEmbedding K (x : 𝓞 K) ∈ integerSet K := by + refine exists_unitSMul_mem_integerSet ?_ ⟨(x : 𝓞 K), Set.mem_range_self _, rfl⟩ exact (map_ne_zero _).mpr <| RingOfIntegers.coe_ne_zero_iff.mpr (nonZeroDivisors.coe_ne_zero _) refine ⟨⟨u • mixedEmbedding K (x : 𝓞 K), hu⟩, Quotient.sound ⟨unitsNonZeroDivisorsEquiv.symm u⁻¹, ?_⟩⟩ simp_rw [Subtype.ext_iff, RingOfIntegers.ext_iff, ← (mixedEmbedding_injective K).eq_iff, - Submonoid.coe_mul, map_mul, mixedEmbedding_preimageOfIntegralPoint, + Submonoid.coe_mul, map_mul, mixedEmbedding_preimageOfMemIntegerSet, unitSMul_smul, ← map_mul, mul_comm, map_inv, val_inv_unitsNonZeroDivisorsEquiv_symm_apply_coe, Units.mul_inv_cancel_right] -theorem integralPointToAssociates_eq_iff (a b : integralPoint K) : - integralPointToAssociates K a = integralPointToAssociates K b ↔ +theorem integerSetToAssociates_eq_iff (a b : integerSet K) : + integerSetToAssociates K a = integerSetToAssociates K b ↔ ∃ ζ : torsion K, ζ • a = b := by - simp_rw [integralPointToAssociates_apply, Associates.quotient_mk_eq_mk, + simp_rw [integerSetToAssociates_apply, Associates.quotient_mk_eq_mk, Associates.mk_eq_mk_iff_associated, Associated, mul_comm, Subtype.ext_iff, RingOfIntegers.ext_iff, ← (mixedEmbedding_injective K).eq_iff, Submonoid.coe_mul, map_mul, - mixedEmbedding_preimageOfIntegralPoint, integralPoint_torsionSMul_smul_coe] + mixedEmbedding_preimageOfMemIntegerSet, integerSetTorsionSMul_smul_coe] refine ⟨fun ⟨u, h⟩ ↦ ⟨⟨unitsNonZeroDivisorsEquiv u, ?_⟩, by simpa using h⟩, fun ⟨⟨u, _⟩, h⟩ ↦ ⟨unitsNonZeroDivisorsEquiv.symm u, by simpa using h⟩⟩ exact (unit_smul_mem_iff_mem_torsion a.prop.1 _).mp (by simpa [h] using b.prop.1) variable (K) in -/-- The equivalence between `integralPoint K` modulo `torsion K` and `Associates (𝓞 K)⁰`. -/ -def integralPointQuotEquivAssociates : - Quotient (MulAction.orbitRel (torsion K) (integralPoint K)) ≃ Associates (𝓞 K)⁰ := +/-- The equivalence between `integerSet K` modulo `torsion K` and `Associates (𝓞 K)⁰`. -/ +def integerSetQuotEquivAssociates : + Quotient (MulAction.orbitRel (torsion K) (integerSet K)) ≃ Associates (𝓞 K)⁰ := Equiv.ofBijective - (Quotient.lift (integralPointToAssociates K) - fun _ _ h ↦ ((integralPointToAssociates_eq_iff _ _).mpr h).symm) - ⟨by convert Setoid.ker_lift_injective (integralPointToAssociates K) + (Quotient.lift (integerSetToAssociates K) + fun _ _ h ↦ ((integerSetToAssociates_eq_iff _ _).mpr h).symm) + ⟨by convert Setoid.ker_lift_injective (integerSetToAssociates K) all_goals · ext a b - rw [Setoid.ker_def, eq_comm, integralPointToAssociates_eq_iff b a, + rw [Setoid.ker_def, eq_comm, integerSetToAssociates_eq_iff b a, MulAction.orbitRel_apply, MulAction.mem_orbit_iff], - (Quot.surjective_lift _).mpr (integralPointToAssociates_surjective K)⟩ + (Quot.surjective_lift _).mpr (integerSetToAssociates_surjective K)⟩ @[simp] -theorem integralPointQuotEquivAssociates_apply (a : integralPoint K) : - integralPointQuotEquivAssociates K ⟦a⟧ = ⟦preimageOfIntegralPoint a⟧ := rfl +theorem integerSetQuotEquivAssociates_apply (a : integerSet K) : + integerSetQuotEquivAssociates K ⟦a⟧ = ⟦preimageOfMemIntegerSet a⟧ := rfl -theorem integralPoint_torsionSMul_stabilizer (a : integralPoint K) : +theorem integerSetTorsionSMul_stabilizer (a : integerSet K) : MulAction.stabilizer (torsion K) a = ⊥ := by refine (Subgroup.eq_bot_iff_forall _).mpr fun ζ hζ ↦ ?_ - rwa [MulAction.mem_stabilizer_iff, Subtype.ext_iff, integralPoint_torsionSMul_smul_coe, - unitSMul_smul, ← mixedEmbedding_preimageOfIntegralPoint, ← map_mul, + rwa [MulAction.mem_stabilizer_iff, Subtype.ext_iff, integerSetTorsionSMul_smul_coe, + unitSMul_smul, ← mixedEmbedding_preimageOfMemIntegerSet, ← map_mul, (mixedEmbedding_injective K).eq_iff, ← map_mul, ← RingOfIntegers.ext_iff, mul_eq_right₀, Units.val_eq_one, OneMemClass.coe_eq_one] at hζ exact nonZeroDivisors.coe_ne_zero _ @@ -407,93 +404,190 @@ theorem integralPoint_torsionSMul_stabilizer (a : integralPoint K) : open Submodule Ideal variable (K) in -/-- The equivalence between `integralPoint K` and the product of the set of nonzero principal +/-- The equivalence between `integerSet K` and the product of the set of nonzero principal ideals of `K` and the torsion of `K`. -/ -def integralPointEquiv : - integralPoint K ≃ {I : (Ideal (𝓞 K))⁰ // IsPrincipal I.val} × torsion K := - (MulAction.selfEquivSigmaOrbitsQuotientStabilizer (torsion K) (integralPoint K)).trans +def integerSetEquiv : + integerSet K ≃ {I : (Ideal (𝓞 K))⁰ // IsPrincipal I.val} × torsion K := + (MulAction.selfEquivSigmaOrbitsQuotientStabilizer (torsion K) (integerSet K)).trans ((Equiv.sigmaEquivProdOfEquiv (by intro _ - simp_rw [integralPoint_torsionSMul_stabilizer] + simp_rw [integerSetTorsionSMul_stabilizer] exact QuotientGroup.quotientBot.toEquiv)).trans - (Equiv.prodCongrLeft (fun _ ↦ (integralPointQuotEquivAssociates K).trans + (Equiv.prodCongrLeft (fun _ ↦ (integerSetQuotEquivAssociates K).trans (Ideal.associatesNonZeroDivisorsEquivIsPrincipal (𝓞 K))))) @[simp] -theorem integralPointEquiv_apply_fst (a : integralPoint K) : - ((integralPointEquiv K a).1 : Ideal (𝓞 K)) = span {(preimageOfIntegralPoint a : 𝓞 K)} := rfl +theorem integerSetEquiv_apply_fst (a : integerSet K) : + ((integerSetEquiv K a).1 : Ideal (𝓞 K)) = span {(preimageOfMemIntegerSet a : 𝓞 K)} := rfl variable (K) in -/-- For an integer `n`, The equivalence between the `integralPoint K` of norm `n` and the product -of the set of nonzero principal ideals of `K` of norm `n` and the torsion of `K`. -/ -def integralPointEquivNorm (n : ℕ) : - {a : integralPoint K // intNorm a = n} ≃ +/-- For an integer `n`, The equivalence between the elements of `integerSet K` of norm `n` +and the product of the set of nonzero principal ideals of `K` of norm `n` and the torsion of `K`. -/ +def integerSetEquivNorm (n : ℕ) : + {a : integerSet K // mixedEmbedding.norm (a : mixedSpace K) = n} ≃ {I : (Ideal (𝓞 K))⁰ // IsPrincipal (I : Ideal (𝓞 K)) ∧ absNorm (I : Ideal (𝓞 K)) = n} × (torsion K) := - calc {a // intNorm a = n} - ≃ {I : {I : (Ideal (𝓞 K))⁰ // IsPrincipal I.1} × torsion K // + calc + _ ≃ {I : {I : (Ideal (𝓞 K))⁰ // IsPrincipal I.1} × torsion K // absNorm (I.1 : Ideal (𝓞 K)) = n} := - (Equiv.subtypeEquiv (integralPointEquiv K) fun _ ↦ by simp [intNorm, absNorm_span_singleton]) + Equiv.subtypeEquiv (integerSetEquiv K) fun _ ↦ by simp_rw [← intNorm_coe, intNorm, + Nat.cast_inj, integerSetEquiv_apply_fst, absNorm_span_singleton] _ ≃ {I : {I : (Ideal (𝓞 K))⁰ // IsPrincipal I.1} // absNorm (I.1 : Ideal (𝓞 K)) = n} × - torsion K := - Equiv.prodSubtypeFstEquivSubtypeProd (p := fun I : {I : (Ideal (𝓞 K))⁰ // IsPrincipal I.1} ↦ - absNorm (I : Ideal (𝓞 K)) = n) + torsion K := Equiv.prodSubtypeFstEquivSubtypeProd + (p := fun I : {I : (Ideal (𝓞 K))⁰ // IsPrincipal I.1} ↦ absNorm (I : Ideal (𝓞 K)) = n) _ ≃ {I : (Ideal (𝓞 K))⁰ // IsPrincipal (I : Ideal (𝓞 K)) ∧ - absNorm (I : Ideal (𝓞 K)) = n} × (torsion K) := - Equiv.prodCongrLeft fun _ ↦ (Equiv.subtypeSubtypeEquivSubtypeInter + absNorm (I : Ideal (𝓞 K)) = n} × (torsion K) := Equiv.prodCongrLeft fun _ ↦ + (Equiv.subtypeSubtypeEquivSubtypeInter (fun I : (Ideal (𝓞 K))⁰ ↦ IsPrincipal I.1) (fun I ↦ absNorm I.1 = n)) @[simp] -theorem integralPointEquivNorm_apply_fst {n : ℕ} {a : integralPoint K} (ha : intNorm a = n) : - ((integralPointEquivNorm K n ⟨a, ha⟩).1 : Ideal (𝓞 K)) = - span {(preimageOfIntegralPoint a : 𝓞 K)} := by - simp_rw [integralPointEquivNorm, Equiv.prodSubtypeFstEquivSubtypeProd, Equiv.instTrans_trans, - Equiv.prodCongrLeft, Equiv.trans_apply, Equiv.subtypeEquiv_apply, Equiv.coe_fn_mk, - Equiv.subtypeSubtypeEquivSubtypeInter_apply_coe, integralPointEquiv_apply_fst] +theorem integerSetEquivNorm_apply_fst {n : ℕ} + (a : {a : integerSet K // mixedEmbedding.norm (a : mixedSpace K) = n}) : + ((integerSetEquivNorm K n a).1 : Ideal (𝓞 K)) = + span {(preimageOfMemIntegerSet a.val : 𝓞 K)} := by + simp_rw [integerSetEquivNorm, Equiv.prodSubtypeFstEquivSubtypeProd, Equiv.instTrans_trans, + Equiv.prodCongrLeft, Equiv.trans_apply, Equiv.subtypeEquiv_apply, Equiv.coe_fn_mk, + Equiv.subtypeSubtypeEquivSubtypeInter_apply_coe, integerSetEquiv_apply_fst] variable (K) /-- For `n` positive, the number of principal ideals in `𝓞 K` of norm `n` multiplied by the order -of the torsion of `K` is equal to the number of `integralPoint K` of norm `n`. -/ +of the torsion of `K` is equal to the number of elements in `integerSet K` of norm `n`. -/ theorem card_isPrincipal_norm_eq_mul_torsion (n : ℕ) : Nat.card {I : (Ideal (𝓞 K))⁰ | IsPrincipal (I : Ideal (𝓞 K)) ∧ absNorm (I : Ideal (𝓞 K)) = n} * torsionOrder K = - Nat.card {a : integralPoint K | intNorm a = n} := by + Nat.card {a : integerSet K | mixedEmbedding.norm (a : mixedSpace K) = n} := by rw [torsionOrder, PNat.mk_coe, ← Nat.card_eq_fintype_card, ← Nat.card_prod] - exact Nat.card_congr (integralPointEquivNorm K n).symm + exact Nat.card_congr (integerSetEquivNorm K n).symm + +variable (J : (Ideal (𝓞 K))⁰) + +/-- The intersection between the fundamental cone and the `idealLattice` defined by the image of +the integral ideal `J`. -/ +def idealSet : Set (mixedSpace K) := + fundamentalCone K ∩ (mixedEmbedding.idealLattice K (FractionalIdeal.mk0 K J)) + +variable {K J} in +theorem mem_idealSet : + x ∈ idealSet K J ↔ x ∈ fundamentalCone K ∧ ∃ a : (𝓞 K), (a : 𝓞 K) ∈ (J : Set (𝓞 K)) ∧ + mixedEmbedding K (a : 𝓞 K) = x := by + simp_rw [idealSet, Set.mem_inter_iff, idealLattice, SetLike.mem_coe, FractionalIdeal.coe_mk0, + LinearMap.mem_range, LinearMap.coe_comp, LinearMap.coe_restrictScalars, coe_subtype, + Function.comp_apply, AlgHom.toLinearMap_apply, RingHom.toIntAlgHom_coe, Subtype.exists, + FractionalIdeal.mem_coe, FractionalIdeal.mem_coeIdeal, exists_prop', nonempty_prop, + exists_exists_and_eq_and] + +/-- The map that sends `a : idealSet` to an element of `integerSet`. This map exists because +`J` is an integral ideal. -/ +def idealSetMap : idealSet K J → integerSet K := + fun ⟨a, ha⟩ ↦ ⟨a, mem_integerSet.mpr ⟨(mem_idealSet.mp ha).1, (mem_idealSet.mp ha).2.choose, + (mem_idealSet.mp ha).2.choose_spec.2⟩⟩ -/-- For `s : ℝ`, the number of principal nonzero ideals in `𝓞 K` of norm `≤ s` multiplied by the -order of the torsion of `K` is equal to the number of `integralPoint K` of norm `≤ s`. -/ -theorem card_isPrincipal_norm_le_mul_torsion (s : ℝ) : - Nat.card {I : (Ideal (𝓞 K))⁰ | IsPrincipal (I : Ideal (𝓞 K)) ∧ +@[simp] +theorem idealSetMap_apply (a : idealSet K J) : (idealSetMap K J a : mixedSpace K) = a := rfl + +theorem preimage_of_IdealSetMap (a : idealSet K J) : + (preimageOfMemIntegerSet (idealSetMap K J a) : 𝓞 K) ∈ (J : Set (𝓞 K)) := by + obtain ⟨_, ⟨x, hx₁, hx₂⟩⟩ := mem_idealSet.mp a.prop + simp_rw [idealSetMap, ← hx₂, preimageOfMemIntegerSet_mixedEmbedding] + exact hx₁ + +/-- The map `idealSetMap` is actually an equiv between `idealSet K J` and the elements of +`integerSet K` whose preimage lies in `J`. -/ +def idealSetEquiv : idealSet K J ≃ + {a : integerSet K | (preimageOfMemIntegerSet a : 𝓞 K) ∈ (J : Set (𝓞 K))} := + Equiv.ofBijective (fun a ↦ ⟨idealSetMap K J a, preimage_of_IdealSetMap K J a⟩) + ⟨fun _ _ h ↦ (by + simp_rw [Subtype.ext_iff_val, idealSetMap_apply] at h + rwa [Subtype.ext_iff_val]), + fun ⟨a, ha₂⟩ ↦ ⟨⟨a.val, mem_idealSet.mpr ⟨a.prop.1, + ⟨preimageOfMemIntegerSet a, ha₂, mixedEmbedding_preimageOfMemIntegerSet a⟩⟩⟩, rfl⟩⟩ + +variable {K J} + +theorem idealSetEquiv_apply (a : idealSet K J) : + (idealSetEquiv K J a : mixedSpace K) = a := rfl + +theorem idealSetEquiv_symm_apply + (a : {a : integerSet K // (preimageOfMemIntegerSet a : 𝓞 K) ∈ (J : Set (𝓞 K)) }) : + ((idealSetEquiv K J).symm a : mixedSpace K) = a := by + rw [← (idealSetEquiv_apply ((idealSetEquiv K J).symm a)), Equiv.apply_symm_apply] + +theorem intNorm_idealSetEquiv_apply (a : idealSet K J) : + intNorm (idealSetEquiv K J a).val = mixedEmbedding.norm (a : mixedSpace K) := by + rw [intNorm_coe, idealSetEquiv_apply] + +variable (K J) + +/-- For an integer `n`, The equivalence between the elements of `idealSet K` of norm `n` and +the product of the set of nonzero principal ideals of `K` divisible by `J` of norm `n` and the +torsion of `K`. -/ +def idealSetEquivNorm (n : ℕ) : + {a : idealSet K J // mixedEmbedding.norm (a : mixedSpace K) = n} ≃ + {I : (Ideal (𝓞 K))⁰ // (J : Ideal (𝓞 K)) ∣ I ∧ IsPrincipal (I : Ideal (𝓞 K)) ∧ + absNorm (I : Ideal (𝓞 K)) = n} × (torsion K) := + calc + _ ≃ {a : {a : integerSet K // (preimageOfMemIntegerSet a).1 ∈ J.1} // + mixedEmbedding.norm a.1.1 = n} := by + convert (Equiv.subtypeEquivOfSubtype (idealSetEquiv K J).symm).symm using 3 + rw [idealSetEquiv_symm_apply] + _ ≃ {a : integerSet K // (preimageOfMemIntegerSet a).1 ∈ J.1 ∧ + mixedEmbedding.norm a.1 = n} := Equiv.subtypeSubtypeEquivSubtypeInter + (fun a : integerSet K ↦ (preimageOfMemIntegerSet a).1 ∈ J.1) + (fun a ↦ mixedEmbedding.norm a.1 = n) + _ ≃ {a : {a :integerSet K // mixedEmbedding.norm a.1 = n} // + (preimageOfMemIntegerSet a.1).1 ∈ J.1} := ((Equiv.subtypeSubtypeEquivSubtypeInter + (fun a : integerSet K ↦ mixedEmbedding.norm a.1 = n) + (fun a ↦ (preimageOfMemIntegerSet a).1 ∈ J.1)).trans + (Equiv.subtypeEquivRight (fun _ ↦ by simp [and_comm]))).symm + _ ≃ {I : {I : (Ideal (𝓞 K))⁰ // IsPrincipal I.1 ∧ absNorm I.1 = n} × (torsion K) // + J.1 ∣ I.1.1} := by + convert Equiv.subtypeEquivOfSubtype (p := fun I ↦ J.1 ∣ I.1) (integerSetEquivNorm K n) + rw [integerSetEquivNorm_apply_fst, dvd_span_singleton] + _ ≃ {I : {I : (Ideal (𝓞 K))⁰ // IsPrincipal I.1 ∧ absNorm I.1 = n} // J.1 ∣ I.1} × + (torsion K) := Equiv.prodSubtypeFstEquivSubtypeProd + (p := fun I : {I : (Ideal (𝓞 K))⁰ // IsPrincipal I.1 ∧ absNorm I.1 = n} ↦ J.1 ∣ I.1) + _ ≃ {I : (Ideal (𝓞 K))⁰ // (IsPrincipal I.1 ∧ absNorm I.1 = n) ∧ J.1 ∣ I.1} × (torsion K) := + Equiv.prodCongrLeft fun _ ↦ (Equiv.subtypeSubtypeEquivSubtypeInter + (fun I : (Ideal (𝓞 K))⁰ ↦ IsPrincipal I.1 ∧ absNorm I.1 = n) + (fun I ↦ J.1 ∣ I.1)) + _ ≃ {I : (Ideal (𝓞 K))⁰ // J.1 ∣ I.1 ∧ IsPrincipal I.1 ∧ absNorm I.1 = n} × + (Units.torsion K) := + Equiv.prodCongrLeft fun _ ↦ Equiv.subtypeEquivRight fun _ ↦ by rw [and_comm] + +/-- For `s : ℝ`, the number of principal nonzero ideals in `𝓞 K` divisible par `J` of norm `≤ s` +multiplied by the order of the torsion of `K` is equal to the number of elements in `idealSet K J` +of norm `≤ s`. -/ +theorem card_isPrincipal_dvd_norm_le (s : ℝ) : + Nat.card {I : (Ideal (𝓞 K))⁰ // (J : Ideal (𝓞 K)) ∣ I ∧ IsPrincipal (I : Ideal (𝓞 K)) ∧ absNorm (I : Ideal (𝓞 K)) ≤ s} * torsionOrder K = - Nat.card {a : integralPoint K | intNorm a ≤ s} := by + Nat.card {a : idealSet K J // mixedEmbedding.norm (a : mixedSpace K) ≤ s} := by obtain hs | hs := le_or_gt 0 s - · simp_rw [← Nat.le_floor_iff hs] + · simp_rw [← intNorm_idealSetEquiv_apply, ← Nat.le_floor_iff hs] rw [torsionOrder, PNat.mk_coe, ← Nat.card_eq_fintype_card, ← Nat.card_prod] - refine Nat.card_congr <| @Equiv.ofFiberEquiv _ (γ := Finset.Iic _) _ - (fun I ↦ ⟨absNorm (I.1 : Ideal (𝓞 K)), Finset.mem_Iic.mpr I.1.2.2⟩) - (fun a ↦ ⟨intNorm a.1, Finset.mem_Iic.mpr a.2⟩) fun ⟨i, hi⟩ ↦ ?_ + refine Nat.card_congr <| @Equiv.ofFiberEquiv _ (γ := Finset.Iic ⌊s⌋₊) _ + (fun I ↦ ⟨absNorm I.1.val.1, Finset.mem_Iic.mpr I.1.prop.2.2⟩) + (fun a ↦ ⟨intNorm (idealSetEquiv K J a.1).1, Finset.mem_Iic.mpr a.prop⟩) fun ⟨i, hi⟩ ↦ ?_ simp_rw [Subtype.mk.injEq] - calc - _ ≃ {I : {I : (Ideal (𝓞 K))⁰ // IsPrincipal I.1 ∧ absNorm I.1 ≤ _} // absNorm I.1.1 = i} - × torsion K := Equiv.prodSubtypeFstEquivSubtypeProd - _ ≃ {I : (Ideal (𝓞 K))⁰ // (IsPrincipal I.1 ∧ absNorm I.1 ≤ _) ∧ absNorm I.1 = i} - × torsion K := - Equiv.prodCongrLeft fun _ ↦ (Equiv.subtypeSubtypeEquivSubtypeInter - (p := fun I : (Ideal (𝓞 K))⁰ ↦ IsPrincipal I.1 ∧ absNorm I.1 ≤ _) + calc _ ≃ {I : {I : (Ideal (𝓞 K))⁰ // _ ∧ _ ∧ _} // absNorm I.1.1 = i} × torsion K := + Equiv.prodSubtypeFstEquivSubtypeProd + _ ≃ {I : (Ideal (𝓞 K))⁰ // (_ ∧ _ ∧ absNorm I.1 ≤ ⌊s⌋₊) ∧ absNorm I.1 = i} + × torsion K := Equiv.prodCongrLeft fun _ ↦ (Equiv.subtypeSubtypeEquivSubtypeInter + (p := fun I : (Ideal (𝓞 K))⁰ ↦ J.1 ∣ I.1 ∧ IsPrincipal I.1 ∧ absNorm I.1 ≤ ⌊s⌋₊) (q := fun I ↦ absNorm I.1 = i)) - _ ≃ {I : (Ideal (𝓞 K))⁰ // IsPrincipal I.1 ∧ absNorm I.1 = i ∧ absNorm I.1 ≤ _} - × torsion K := - Equiv.prodCongrLeft fun _ ↦ (Equiv.subtypeEquivRight fun _ ↦ by aesop) - _ ≃ {I : (Ideal (𝓞 K))⁰ // IsPrincipal I.1 ∧ absNorm I.1 = i} × torsion K := - Equiv.prodCongrLeft fun _ ↦ (Equiv.subtypeEquivRight fun _ ↦ by - rw [and_iff_left_of_imp (a := absNorm _ = _) fun h ↦ Finset.mem_Iic.mp (h ▸ hi)]) - _ ≃ {a : integralPoint K // intNorm a = i} := (integralPointEquivNorm K i).symm - _ ≃ {a : {a : integralPoint K // intNorm a ≤ _} // intNorm a.1 = i} := - (Equiv.subtypeSubtypeEquivSubtype fun h ↦ Finset.mem_Iic.mp (h ▸ hi)).symm - · simp_rw [lt_iff_not_le.mp (lt_of_lt_of_le hs (Nat.cast_nonneg _)), and_false, Set.setOf_false, - Nat.card_eq_fintype_card, Fintype.card_ofIsEmpty, zero_mul] + _ ≃ {I : (Ideal (𝓞 K))⁰ // J.1 ∣ I.1 ∧ IsPrincipal I.1 ∧ absNorm I.1 = i} + × torsion K := Equiv.prodCongrLeft fun _ ↦ Equiv.subtypeEquivRight fun _ ↦ by aesop + _ ≃ {a : idealSet K J // mixedEmbedding.norm (a : mixedSpace K) = i} := + (idealSetEquivNorm K J i).symm + _ ≃ {a : idealSet K J // intNorm (idealSetEquiv K J a).1 = i} := by + simp_rw [← intNorm_idealSetEquiv_apply, Nat.cast_inj] + rfl + _ ≃ {b : {a : idealSet K J // intNorm (idealSetEquiv K J a).1 ≤ ⌊s⌋₊} // + intNorm (idealSetEquiv K J b).1 = i} := + (Equiv.subtypeSubtypeEquivSubtype fun h ↦ Finset.mem_Iic.mp (h ▸ hi)).symm + · simp_rw [lt_iff_not_le.mp (lt_of_lt_of_le hs (Nat.cast_nonneg _)), lt_iff_not_le.mp + (lt_of_lt_of_le hs (mixedEmbedding.norm_nonneg _)), and_false, Nat.card_of_isEmpty, + zero_mul] end fundamentalCone