FreeLatticeCard110.lean

1 import Mathlib.LinearAlgebra.Quotient.Pi
2 import Mathlib.LinearAlgebra.Basis.Defs
3 import Mathlib.RingTheory.Ideal.Norm.AbsNorm
4 import Mathlib.RingTheory.Ideal.Operations
5 
6 /-! Cardinality of ideal quotients of an actual finite free module.
7 This supplies the numerical lattice leaf once its corner basis is constructed;
8 it does not assert that an arbitrary additive lattice has that basis. -/
9 set_option autoImplicit false
10 noncomputable section
11 namespace PaperXI.FreeLatticeCard110
12 
13 variable {R M ι : Type*} [CommRing R] [AddCommGroup M] [Module R M]
14   [Fintype ι] [DecidableEq ι]
15 
16 theorem ideal_smul_top_pi (I : Ideal R) :
17     I • (⊤ : Submodule R (ι → R)) = Submodule.pi Set.univ (fun _ : ι => I) := by
18   apply le_antisymm
19   · apply Submodule.smul_le.mpr
20     intro r hr f _
21     apply Submodule.mem_pi.mpr
22     intro i _
23     exact I.mul_mem_right (f i) hr
24   · intro f hf
25     have hfi : ∀ i, f i ∈ I := fun i => Submodule.mem_pi.mp hf i (Set.mem_univ i)
26     have he : f = ∑ i : ι, f i • Pi.single i (1 : R) := by
27       ext j
28       simp [Pi.single_apply, mul_ite]
29     rw [he]
30     apply Submodule.sum_mem
31     intro i _
32     exact Submodule.smul_mem_smul (hfi i) Submodule.mem_top
33 
34 def quotientEquiv (b : Module.Basis ι R M) (I : Ideal R) :
35     (M ⧸ (I • (⊤ : Submodule R M))) ≃ₗ[R] (ι → R ⧸ I) :=
36   (Submodule.Quotient.equiv _ _ b.equivFun (by
37     rw [Submodule.map_smul'', Submodule.map_top,
38       LinearMap.range_eq_top.mpr b.equivFun.surjective, ideal_smul_top_pi])).trans
39     (Submodule.quotientPi (fun _ : ι => I))
40 
41 theorem card_quotient (b : Module.Basis ι R M) (I : Ideal R) :
42     Nat.card (M ⧸ (I • (⊤ : Submodule R M))) = Nat.card (R ⧸ I) ^ Fintype.card ι := by
43   rw [Nat.card_congr (quotientEquiv b I).toEquiv, Nat.card_fun]
44   simp only [Nat.card_eq_fintype_card]
45 
46 theorem card_quotient_prime_pow [IsDedekindDomain R] (b : Module.Basis ι R M)
47     (I : Ideal R) [I.IsPrime] (hI : I ≠ ⊥) (a : ℕ) :
48     Nat.card (M ⧸ ((I ^ a) • (⊤ : Submodule R M))) =
49       Nat.card (R ⧸ I) ^ (a * Fintype.card ι) := by
50   rw [card_quotient b (I ^ a)]
51   change (Submodule.cardQuot (I ^ a)) ^ Fintype.card ι = _
52   rw [cardQuot_pow_of_prime hI, ← pow_mul]
53   rfl
54 
55 end PaperXI.FreeLatticeCard110

Back to source controls