MoritaQuotient110.lean

1 import Mathlib.GroupTheory.QuotientGroup.Basic
2 import Mathlib.SetTheory.Cardinal.Finite
3 import PaperXI.MoritaLattice110
4 
5 /-! Actual product quotients for the entrywise Morita calculation.
6 The additive equivalences are constructed from coordinate quotient maps,
7 their proved kernels, and proved surjectivity. The cardinality conclusions
8 are consequences of those equivalences, with no supplied index formula. -/
9 set_option autoImplicit false
10 noncomputable section
11 namespace PaperXI.MoritaQuotient110
12 
13 variable {ι : Type*} {G : ι → Type*} [∀ i, AddCommGroup (G i)]
14 
15 /-- The map to the product of the literal coordinate quotients. -/
16 def coordinateQuotientMap (K : ∀ i, AddSubgroup (G i)) :
17     (∀ i, G i) →+ (∀ i, G i ⧸ K i) where
18   toFun x i := (x i : G i ⧸ K i)
19   map_zero' := by ext i; exact map_zero (QuotientAddGroup.mk' (K i))
20   map_add' x y := by ext i; exact map_add (QuotientAddGroup.mk' (K i)) (x i) (y i)
21 
22 @[simp] theorem coordinateQuotientMap_apply (K : ∀ i, AddSubgroup (G i))
23     (x : ∀ i, G i) (i : ι) :
24     coordinateQuotientMap K x i = (x i : G i ⧸ K i) := rfl
25 
26 /-- Every coordinate quotient has a representative; choice assembles them. -/
27 theorem coordinateQuotientMap_surjective (K : ∀ i, AddSubgroup (G i)) :
28     Function.Surjective (coordinateQuotientMap K) := by
29   intro y
30   refine ⟨fun i => Quotient.out (y i), ?_⟩
31   ext i
32   exact Quotient.out_eq (y i)
33 
34 /-- Its kernel is exactly the product subgroup. -/
35 theorem coordinateQuotientMap_ker (K : ∀ i, AddSubgroup (G i)) :
36     (coordinateQuotientMap K).ker = AddSubgroup.pi Set.univ K := by
37   ext x
38   simp only [AddMonoidHom.mem_ker, funext_iff, coordinateQuotientMap_apply,
39     Pi.zero_apply, QuotientAddGroup.eq_zero_iff, AddSubgroup.mem_pi,
40     Set.mem_univ, forall_const]
41 
42 /-- The quotient of a dependent product is the product of its quotients. -/
43 def piQuotientEquiv (K : ∀ i, AddSubgroup (G i)) :
44     ((∀ i, G i) ⧸ AddSubgroup.pi Set.univ K) ≃+ (∀ i, G i ⧸ K i) :=
45   QuotientAddGroup.liftEquiv (AddSubgroup.pi Set.univ K)
46     (coordinateQuotientMap_surjective K) (coordinateQuotientMap_ker K).symm
47 
48 @[simp] theorem piQuotientEquiv_mk (K : ∀ i, AddSubgroup (G i))
49     (x : ∀ i, G i) (i : ι) :
50     piQuotientEquiv K (x : (∀ i, G i) ⧸ AddSubgroup.pi Set.univ K) i =
51       (x i : G i ⧸ K i) := rfl
52 
53 /-- The cardinality formula follows from the actual additive equivalence. -/
54 theorem card_pi_quotient [Fintype ι] (K : ∀ i, AddSubgroup (G i)) :
55     Nat.card ((∀ i, G i) ⧸ AddSubgroup.pi Set.univ K) =
56       ∏ i, Nat.card (G i ⧸ K i) := by
57   rw [Nat.card_congr (piQuotientEquiv K).toEquiv, Nat.card_pi]
58 
59 /-- The actual product subgroup maps to its coordinate subgroup quotients. -/
60 def subgroupCoordinateQuotientMap (L K : ∀ i, AddSubgroup (G i)) :
61     AddSubgroup.pi Set.univ L →+ (∀ i, L i ⧸ (K i).addSubgroupOf (L i)) where
62   toFun x i := (⟨x.1 i, x.2 i (Set.mem_univ i)⟩ : L i)
63   map_zero' := by ext i; rfl
64   map_add' x y := by ext i; rfl
65 
66 @[simp] theorem subgroupCoordinateQuotientMap_apply
67     (L K : ∀ i, AddSubgroup (G i)) (x : AddSubgroup.pi Set.univ L) (i : ι) :
68     subgroupCoordinateQuotientMap L K x i =
69       ((⟨x.1 i, x.2 i (Set.mem_univ i)⟩ : L i) : L i ⧸ (K i).addSubgroupOf (L i)) := rfl
70 
71 /-- Representatives in each actual subgroup assemble to a product element. -/
72 theorem subgroupCoordinateQuotientMap_surjective
73     (L K : ∀ i, AddSubgroup (G i)) :
74     Function.Surjective (subgroupCoordinateQuotientMap L K) := by
75   intro y
76   let x : ∀ i, L i := fun i => Quotient.out (y i)
77   refine ⟨⟨fun i => (x i : G i), fun i _ => (x i).2⟩, ?_⟩
78   ext i
79   exact Quotient.out_eq (y i)
80 
81 /-- The kernel is the literal smaller product viewed inside the larger one. -/
82 theorem subgroupCoordinateQuotientMap_ker (L K : ∀ i, AddSubgroup (G i)) :
83     (subgroupCoordinateQuotientMap L K).ker =
84       (AddSubgroup.pi Set.univ K).addSubgroupOf (AddSubgroup.pi Set.univ L) := by
85   ext x
86   simp only [AddMonoidHom.mem_ker, funext_iff, subgroupCoordinateQuotientMap_apply,
87     Pi.zero_apply, QuotientAddGroup.eq_zero_iff, AddSubgroup.mem_addSubgroupOf,
88     AddSubgroup.mem_pi, Set.mem_univ, forall_const]
89 
90 /-- The actual ambient product-subgroup quotient splits by coordinates.
91 When `K i ≤ L i`, the denominator is exactly the intended smaller lattice;
92 the statement also remains valid for arbitrary `K`, via `addSubgroupOf`. -/
93 def subgroupPiQuotientEquiv (L K : ∀ i, AddSubgroup (G i)) :
94     (AddSubgroup.pi Set.univ L ⧸
95       (AddSubgroup.pi Set.univ K).addSubgroupOf (AddSubgroup.pi Set.univ L)) ≃+
96         (∀ i, L i ⧸ (K i).addSubgroupOf (L i)) :=
97   QuotientAddGroup.liftEquiv
98     ((AddSubgroup.pi Set.univ K).addSubgroupOf (AddSubgroup.pi Set.univ L))
99     (subgroupCoordinateQuotientMap_surjective L K)
100     (subgroupCoordinateQuotientMap_ker L K).symm
101 
102 @[simp] theorem subgroupPiQuotientEquiv_mk (L K : ∀ i, AddSubgroup (G i))
103     (x : AddSubgroup.pi Set.univ L) (i : ι) :
104     subgroupPiQuotientEquiv L K
105       (x : AddSubgroup.pi Set.univ L ⧸
106         (AddSubgroup.pi Set.univ K).addSubgroupOf (AddSubgroup.pi Set.univ L)) i =
107       ((⟨x.1 i, x.2 i (Set.mem_univ i)⟩ : L i) : L i ⧸ (K i).addSubgroupOf (L i)) := rfl
108 
109 /-- The index cardinality of actual product lattices is the coordinate product. -/
110 theorem card_subgroup_pi_quotient [Fintype ι] (L K : ∀ i, AddSubgroup (G i)) :
111     Nat.card (AddSubgroup.pi Set.univ L ⧸
112       (AddSubgroup.pi Set.univ K).addSubgroupOf (AddSubgroup.pi Set.univ L)) =
113         ∏ i, Nat.card (L i ⧸ (K i).addSubgroupOf (L i)) := by
114   rw [Nat.card_congr (subgroupPiQuotientEquiv L K).toEquiv, Nat.card_pi]
115 
116 section Matrix
117 variable {D m : Type*} [Ring D]
118 open PaperXI.MoritaLattice110
119 
120 /-- The quotient map on the actual matrix subgroup, evaluated entry by entry. -/
121 def matrixCoordinateQuotientMap (L K : m → m → AddSubgroup D) :
122     entrywise L →+ (∀ i j, L i j ⧸ (K i j).addSubgroupOf (L i j)) where
123   toFun x i j := (⟨x.1 i j, x.2 i j⟩ : L i j)
124   map_zero' := by ext i j; rfl
125   map_add' x y := by ext i j; rfl
126 
127 @[simp] theorem matrixCoordinateQuotientMap_apply (L K : m → m → AddSubgroup D)
128     (x : entrywise L) (i j : m) :
129     matrixCoordinateQuotientMap L K x i j =
130       ((⟨x.1 i j, x.2 i j⟩ : L i j) : L i j ⧸ (K i j).addSubgroupOf (L i j)) := rfl
131 
132 theorem matrixCoordinateQuotientMap_surjective (L K : m → m → AddSubgroup D) :
133     Function.Surjective (matrixCoordinateQuotientMap L K) := by
134   intro y
135   let x : ∀ i j, L i j := fun i j => Quotient.out (y i j)
136   refine ⟨⟨fun i j => (x i j : D), fun i j => (x i j).2⟩, ?_⟩
137   ext i j
138   exact Quotient.out_eq (y i j)
139 
140 /-- The kernel is the actual allowed-entry matrix subgroup in the numerator. -/
141 theorem matrixCoordinateQuotientMap_ker (L K : m → m → AddSubgroup D) :
142     (matrixCoordinateQuotientMap L K).ker = (entrywise K).addSubgroupOf (entrywise L) := by
143   ext x
144   simp only [AddMonoidHom.mem_ker, funext_iff, matrixCoordinateQuotientMap_apply,
145     Pi.zero_apply, QuotientAddGroup.eq_zero_iff, AddSubgroup.mem_addSubgroupOf,
146     mem_entrywise]
147 
148 /-- The literal matrix quotient is additively equivalent to its entry quotients. -/
149 def matrixQuotientEquiv (L K : m → m → AddSubgroup D) :
150     (entrywise L ⧸ (entrywise K).addSubgroupOf (entrywise L)) ≃+
151       (∀ i j, L i j ⧸ (K i j).addSubgroupOf (L i j)) :=
152   QuotientAddGroup.liftEquiv ((entrywise K).addSubgroupOf (entrywise L))
153     (matrixCoordinateQuotientMap_surjective L K) (matrixCoordinateQuotientMap_ker L K).symm
154 
155 @[simp] theorem matrixQuotientEquiv_mk (L K : m → m → AddSubgroup D)
156     (x : entrywise L) (i j : m) :
157     matrixQuotientEquiv L K
158       (x : entrywise L ⧸ (entrywise K).addSubgroupOf (entrywise L)) i j =
159         ((⟨x.1 i j, x.2 i j⟩ : L i j) : L i j ⧸ (K i j).addSubgroupOf (L i j)) := rfl
160 
161 /-- The matrix-lattice index cardinality is the product of the entry cardinalities. -/
162 theorem card_matrix_quotient [Fintype m] (L K : m → m → AddSubgroup D) :
163     Nat.card (entrywise L ⧸ (entrywise K).addSubgroupOf (entrywise L)) =
164       ∏ i, ∏ j, Nat.card (L i j ⧸ (K i j).addSubgroupOf (L i j)) := by
165   rw [Nat.card_congr (matrixQuotientEquiv L K).toEquiv]
166   simp_rw [Nat.card_pi]
167 
168 end Matrix
169 
170 end PaperXI.MoritaQuotient110

Back to source controls