CyclicFiniteTargets.lean

1 import RealizationBoundaries.CyclicQuotients
2 import RealizationBoundaries.FiniteTargets
3 import Mathlib.GroupTheory.SpecificGroups.Cyclic
4 import Mathlib.Data.Nat.Squarefree
5 
6 /-! # Exact classification of finite quotient targets
7 
8 Every finite quotient, not only the displayed canonical quotients, is cyclic of
9 squarefree order. Conversely every finite cyclic squarefree target occurs. A
10 surjective map's kernel is the actual multiple subgroup indexed by target order.
11 -/
12 set_option autoImplicit false
13 noncomputable section
14 open scoped BigOperators
15 namespace RealizationBoundaries
16 
17 theorem primeRadical_squarefree (m : ℕ) : Squarefree (primeRadical m) := by
18   apply Finset.squarefree_prod_of_pairwise_isCoprime
19   · intro p hp q hq hpq
20     exact Nat.coprime_iff_isRelPrime.mp
21       ((Nat.coprime_primes (Nat.prime_of_mem_primeFactors hp)
22         (Nat.prime_of_mem_primeFactors hq)).mpr hpq)
23   · intro p hp
24     exact (Nat.prime_of_mem_primeFactors hp).prime.squarefree
25 
26 theorem primeRadical_eq_of_squarefree {m : ℕ} (hm : Squarefree m) : primeRadical m = m :=
27   Nat.prod_primeFactors_of_squarefree hm
28 
29 variable (W : Submodule ℚ TailSpace) (F : Type*) [AddGroup F] [Finite F]
30 
31 /-- A factor through the actual cyclic radical quotient for every finite-target map. -/
32 def finiteTargetCyclicFactor (f : preimage W →+ F) : ZMod (primeRadical (Nat.card F)) →+ F :=
33   (finiteTargetFactor W F f).comp (divisorCrtEquiv Nat.card_pos).toAddMonoidHom
34 
35 @[simp] theorem finiteTargetCyclicFactor_quotient (f : preimage W →+ F) (x : preimage W) :
36     finiteTargetCyclicFactor W F f
37       (cyclicIntegerQuotientEquiv W Nat.card_pos (QuotientAddGroup.mk x)) = f x := by
38   change finiteTargetFactor W F f
39     (divisorCrtEquiv Nat.card_pos
40       (cyclicIntegerQuotientEquiv W Nat.card_pos (QuotientAddGroup.mk x))) = _
41   rw [cyclicIntegerQuotientEquiv_mk, finiteTargetFactor_coordinate]
42 
43 theorem finiteTargetCyclicFactor_surjective (f : preimage W →+ F)
44     (hf : Function.Surjective f) : Function.Surjective (finiteTargetCyclicFactor W F f) := by
45   intro z
46   obtain ⟨x, rfl⟩ := hf z
47   exact ⟨cyclicIntegerQuotientEquiv W Nat.card_pos (QuotientAddGroup.mk x),
48     finiteTargetCyclicFactor_quotient W F f x⟩
49 
50 /-- A finite quotient has no repeated prime in its order. -/
51 theorem finite_quotient_radical_card (f : preimage W →+ F) (hf : Function.Surjective f) :
52     primeRadical (Nat.card F) = Nat.card F := by
53   have hpos := primeRadical_pos (Nat.card F)
54   let : NeZero (primeRadical (Nat.card F)) := ⟨Nat.ne_of_gt hpos⟩
55   apply Nat.le_antisymm (Nat.le_of_dvd Nat.card_pos (primeRadical_dvd _))
56   have h := Nat.card_le_card_of_surjective (finiteTargetCyclicFactor W F f)
57     (finiteTargetCyclicFactor_surjective W F f hf)
58   simpa only [Nat.card_eq_fintype_card, ZMod.card] using h
59 
60 theorem finite_quotient_squarefree (f : preimage W →+ F) (hf : Function.Surjective f) :
61     Squarefree (Nat.card F) := by
62   rw [← finite_quotient_radical_card W F f hf]
63   exact primeRadical_squarefree _
64 
65 /-- Cyclicity is derived for the target, even if it was supplied as an arbitrary finite group. -/
66 theorem finite_quotient_cyclic (f : preimage W →+ F) (hf : Function.Surjective f) :
67     IsAddCyclic F :=
68   isAddCyclic_of_surjective (finiteTargetCyclicFactor W F f)
69     (finiteTargetCyclicFactor_surjective W F f hf)
70 
71 /-- With a surjective original map, the full divisor-coordinate factor is bijective. -/
72 theorem finiteTargetFactor_bijective (f : preimage W →+ F) (hf : Function.Surjective f) :
73     Function.Bijective (finiteTargetFactor W F f) := by
74   let : Finite (DivisorCoordinates (Nat.card F)) := divisorCoordinates_finite Nat.card_pos
75   apply (Nat.bijective_iff_surjective_and_card _).mpr
76   constructor
77   · intro z
78     obtain ⟨x, rfl⟩ := hf z
79     exact ⟨coordinateMap W (Nat.card F) x, finiteTargetFactor_coordinate W F f x⟩
80   · rw [divisorCoordinates_card Nat.card_pos, finite_quotient_radical_card W F f hf]
81 
82 /-- Target order determines the literal kernel of a finite surjection. -/
83 theorem finite_surjection_ker (f : preimage W →+ F) (hf : Function.Surjective f) :
84     f.ker = multiples W (Nat.card F) := by
85   rw [← coordinateMap_ker W Nat.card_pos]
86   ext x
87   change f x = 0 ↔ coordinateMap W (Nat.card F) x = 0
88   rw [← finiteTargetFactor_coordinate W F f x, ← (finiteTargetFactor W F f).map_zero]
89   exact (finiteTargetFactor_bijective W F f hf).injective.eq_iff
90 
91 /-- Construct a surjection onto any finite cyclic squarefree group. -/
92 def squarefreeCyclicQuotient (hc : IsAddCyclic F) (hs : Squarefree (Nat.card F)) :
93     preimage W →+ F :=
94   ((cyclicIntegerQuotientEquiv W Nat.card_pos).trans
95     ((ZMod.ringEquivCongr (primeRadical_eq_of_squarefree hs)).toAddEquiv.trans
96       (zmodAddCyclicAddEquiv hc))).toAddMonoidHom.comp
97     (QuotientAddGroup.mk' (multiples W (Nat.card F)))
98 
99 theorem squarefreeCyclicQuotient_surjective (hc : IsAddCyclic F)
100     (hs : Squarefree (Nat.card F)) : Function.Surjective (squarefreeCyclicQuotient W F hc hs) := by
101   exact (((cyclicIntegerQuotientEquiv W Nat.card_pos).trans
102     ((ZMod.ringEquivCongr (primeRadical_eq_of_squarefree hs)).toAddEquiv.trans
103       (zmodAddCyclicAddEquiv hc))).surjective).comp (QuotientAddGroup.mk'_surjective _)
104 
105 /-- The full finite-target classification, with an actual surjection in the converse. -/
106 theorem finite_quotient_exists_iff :
107     (∃ f : preimage W →+ F, Function.Surjective f) ↔
108       IsAddCyclic F ∧ Squarefree (Nat.card F) := by
109   constructor
110   · rintro ⟨f, hf⟩
111     exact ⟨finite_quotient_cyclic W F f hf, finite_quotient_squarefree W F f hf⟩
112   · rintro ⟨hc, hs⟩
113     exact ⟨squarefreeCyclicQuotient W F hc hs, squarefreeCyclicQuotient_surjective W F hc hs⟩
114 
115 end RealizationBoundaries

Back to source controls