Yamaguchi Lean 4 Library
ProCGroups/ProC/Category/Pushouts.lean
ProCGroups/ProC/Category/Pushouts/Source

ProCGroups/ProC/Category/Pushouts.lean

1import ProCGroups.ProC.Category.Basic
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/ProCGroups/ProC/Category/Pushouts.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Pro-C groups and open normal quotients
14Defines pro-C conditions from finite group classes, C-open normal subgroups, pro-C categories, products, pullbacks, pushouts, and maximal pro-C quotients.
15-/
17open CategoryTheory
19universe u
21namespace ProCGrp
23variable {ProC : ProCGroups.ProC.ProCGroupPredicate.{u}}
24variable {G G' H H₁ H₂ : ProCGrp ProC}
26/-- A pushout square in the bundled category `ProCGrp ProC`. -/
27def IsPushoutSquare
28 (β₁ : H ⟶ H₁) (β₂ : H ⟶ H₂)
29 (α₁ : H₁ ⟶ G) (α₂ : H₂ ⟶ G) : Prop :=
30 β₁ ≫ α₁ = β₂ ≫ α₂ ∧
31 ∀ ⦃K : ProCGrp ProC⦄ (φ₁ : H₁ ⟶ K) (φ₂ : H₂ ⟶ K),
32 β₁ ≫ φ₁ = β₂ ≫ φ₂ →
33 ∃! φ : G ⟶ K, α₁ ≫ φ = φ₁ ∧ α₂ ≫ φ = φ₂
35/-- Chosen morphism induced by a pro-`C` pushout universal property. -/
36noncomputable def pushoutDesc
37 {β₁ : H ⟶ H₁} {β₂ : H ⟶ H₂}
38 {α₁ : H₁ ⟶ G} {α₂ : H₂ ⟶ G}
39 {K : ProCGrp ProC}
40 (hpo : IsPushoutSquare β₁ β₂ α₁ α₂)
41 (φ₁ : H₁ ⟶ K) (φ₂ : H₂ ⟶ K)
42 (hφ : β₁ ≫ φ₁ = β₂ ≫ φ₂) : G ⟶ K :=
43 Classical.choose (ExistsUnique.exists (hpo.2 φ₁ φ₂ hφ))
45/-- The chosen pushout descent map has the prescribed composites. -/
46theorem pushoutDesc_spec
47 {β₁ : H ⟶ H₁} {β₂ : H ⟶ H₂}
48 {α₁ : H₁ ⟶ G} {α₂ : H₂ ⟶ G}
49 {K : ProCGrp ProC}
50 (hpo : IsPushoutSquare β₁ β₂ α₁ α₂)
51 (φ₁ : H₁ ⟶ K) (φ₂ : H₂ ⟶ K)
52 (hφ : β₁ ≫ φ₁ = β₂ ≫ φ₂) :
53 α₁ ≫ pushoutDesc hpo φ₁ φ₂ hφ = φ₁ ∧
54 α₂ ≫ pushoutDesc hpo φ₁ φ₂ hφ = φ₂ :=
55 Classical.choose_spec (ExistsUnique.exists (hpo.2 φ₁ φ₂ hφ))
57/-- The pushout descent map has the prescribed left composite. -/
58@[simp] theorem pushoutDesc_left
59 {β₁ : H ⟶ H₁} {β₂ : H ⟶ H₂}
60 {α₁ : H₁ ⟶ G} {α₂ : H₂ ⟶ G}
61 {K : ProCGrp ProC}
62 (hpo : IsPushoutSquare β₁ β₂ α₁ α₂)
63 (φ₁ : H₁ ⟶ K) (φ₂ : H₂ ⟶ K)
64 (hφ : β₁ ≫ φ₁ = β₂ ≫ φ₂) :
65 α₁ ≫ pushoutDesc hpo φ₁ φ₂ hφ = φ₁ :=
66 (pushoutDesc_spec hpo φ₁ φ₂ hφ).1
68/-- The pushout descent map has the prescribed right composite. -/
69@[simp] theorem pushoutDesc_right
70 {β₁ : H ⟶ H₁} {β₂ : H ⟶ H₂}
71 {α₁ : H₁ ⟶ G} {α₂ : H₂ ⟶ G}
72 {K : ProCGrp ProC}
73 (hpo : IsPushoutSquare β₁ β₂ α₁ α₂)
74 (φ₁ : H₁ ⟶ K) (φ₂ : H₂ ⟶ K)
75 (hφ : β₁ ≫ φ₁ = β₂ ≫ φ₂) :
76 α₂ ≫ pushoutDesc hpo φ₁ φ₂ hφ = φ₂ :=
77 (pushoutDesc_spec hpo φ₁ φ₂ hφ).2
79/-- Uniqueness of the chosen pushout descent map. -/
81 {β₁ : H ⟶ H₁} {β₂ : H ⟶ H₂}
82 {α₁ : H₁ ⟶ G} {α₂ : H₂ ⟶ G}
83 {K : ProCGrp ProC}
84 (hpo : IsPushoutSquare β₁ β₂ α₁ α₂)
85 (φ₁ : H₁ ⟶ K) (φ₂ : H₂ ⟶ K)
86 (hφ : β₁ ≫ φ₁ = β₂ ≫ φ₂)
87 {ψ : G ⟶ K}
88 (hψ : α₁ ≫ ψ = φ₁ ∧ α₂ ≫ ψ = φ₂) :
89 ψ = pushoutDesc hpo φ₁ φ₂ hφ := by
90 rcases hpo.2 φ₁ φ₂ hφ with ⟨u, hu, huuniq⟩
91 have hψ' : ψ = u := huuniq _ hψ
92 have hdesc : pushoutDesc hpo φ₁ φ₂ hφ = u :=
93 huuniq _ (pushoutDesc_spec hpo φ₁ φ₂ hφ)
94 exact hψ'.trans hdesc.symm
96/-- The self-descent map of a pushout object is the identity. -/
97@[simp] theorem pushoutDesc_self
98 {β₁ : H ⟶ H₁} {β₂ : H ⟶ H₂}
99 {α₁ : H₁ ⟶ G} {α₂ : H₂ ⟶ G}
100 (hpo : IsPushoutSquare β₁ β₂ α₁ α₂) :
101 pushoutDesc hpo α₁ α₂ hpo.1 = 𝟙 G := by
102 symm
103 exact pushoutDesc_unique hpo α₁ α₂ hpo.1 (ψ := 𝟙 G) (by simp only [Category.comp_id, and_self])
105/-- Extensionality of morphisms out of a pro-`C` pushout object. -/
106theorem pushout_hom_ext
107 {β₁ : H ⟶ H₁} {β₂ : H ⟶ H₂}
108 {α₁ : H₁ ⟶ G} {α₂ : H₂ ⟶ G}
109 {K : ProCGrp ProC}
110 (hpo : IsPushoutSquare β₁ β₂ α₁ α₂)
111 {ψ ψ' : G ⟶ K}
112 (h₁ : α₁ ≫ ψ = α₁ ≫ ψ')
113 (h₂ : α₂ ≫ ψ = α₂ ≫ ψ') :
114 ψ = ψ' := by
115 have hφ : β₁ ≫ (α₁ ≫ ψ) = β₂ ≫ (α₂ ≫ ψ) := by
116 calc
117 β₁ ≫ (α₁ ≫ ψ) = (β₁ ≫ α₁) ≫ ψ := by simp only [Category.assoc]
118 _ = (β₂ ≫ α₂) ≫ ψ := by rw [hpo.1]
119 _ = β₂ ≫ (α₂ ≫ ψ) := by simp only [Category.assoc]
120 have hψ :
121 ψ = pushoutDesc hpo (α₁ ≫ ψ) (α₂ ≫ ψ) hφ := by
122 exact pushoutDesc_unique hpo (α₁ ≫ ψ) (α₂ ≫ ψ) hφ (ψ := ψ) ⟨rfl, rfl⟩
123 have hψ' :
124 ψ' = pushoutDesc hpo (α₁ ≫ ψ) (α₂ ≫ ψ) hφ := by
125 exact pushoutDesc_unique hpo (α₁ ≫ ψ) (α₂ ≫ ψ) hφ
126 (ψ := ψ') ⟨h₁.symm, h₂.symm⟩
127 exact hψ.trans hψ'.symm
129/-- Canonical comparison map between two pro-`C` pushout objects of the same cospan. -/
130noncomputable def pushoutMapOfIsPushout
131 {α₁ : H₁ ⟶ G} {α₂ : H₂ ⟶ G}
132 {α₁' : H₁ ⟶ G'} {α₂' : H₂ ⟶ G'}
133 (β₁ : H ⟶ H₁) (β₂ : H ⟶ H₂)
134 (hpo : IsPushoutSquare β₁ β₂ α₁ α₂)
135 (hpo' : IsPushoutSquare β₁ β₂ α₁' α₂') :
136 G ⟶ G' :=
137 pushoutDesc hpo α₁' α₂' hpo'.1
139/-- The comparison map from a pushout object to itself is the identity. -/
140@[simp] theorem pushoutMapOfIsPushout_self
141 {α₁ : H₁ ⟶ G} {α₂ : H₂ ⟶ G}
142 (β₁ : H ⟶ H₁) (β₂ : H ⟶ H₂)
143 (hpo : IsPushoutSquare β₁ β₂ α₁ α₂) :
144 pushoutMapOfIsPushout β₁ β₂ hpo hpo = 𝟙 G := by
145 exact pushoutDesc_self (hpo := hpo)
147/-- The comparison map between pushout objects respects the left structure map. -/
148@[simp] theorem pushoutMapOfIsPushout_left
149 {α₁ : H₁ ⟶ G} {α₂ : H₂ ⟶ G}
150 {α₁' : H₁ ⟶ G'} {α₂' : H₂ ⟶ G'}
151 (β₁ : H ⟶ H₁) (β₂ : H ⟶ H₂)
152 (hpo : IsPushoutSquare β₁ β₂ α₁ α₂)
153 (hpo' : IsPushoutSquare β₁ β₂ α₁' α₂') :
154 α₁ ≫ pushoutMapOfIsPushout β₁ β₂ hpo hpo' = α₁' :=
155 pushoutDesc_left hpo α₁' α₂' hpo'.1
157/-- The comparison map between pushout objects respects the right structure map. -/
158@[simp] theorem pushoutMapOfIsPushout_right
159 {α₁ : H₁ ⟶ G} {α₂ : H₂ ⟶ G}
160 {α₁' : H₁ ⟶ G'} {α₂' : H₂ ⟶ G'}
161 (β₁ : H ⟶ H₁) (β₂ : H ⟶ H₂)
162 (hpo : IsPushoutSquare β₁ β₂ α₁ α₂)
163 (hpo' : IsPushoutSquare β₁ β₂ α₁' α₂') :
164 α₂ ≫ pushoutMapOfIsPushout β₁ β₂ hpo hpo' = α₂' :=
165 pushoutDesc_right hpo α₁' α₂' hpo'.1
167/-- Any two pro-`C` pushout objects of the same cospan are canonically isomorphic. -/
168noncomputable def pushoutIsoOfIsPushout
169 {α₁ : H₁ ⟶ G} {α₂ : H₂ ⟶ G}
170 {α₁' : H₁ ⟶ G'} {α₂' : H₂ ⟶ G'}
171 (β₁ : H ⟶ H₁) (β₂ : H ⟶ H₂)
172 (hpo : IsPushoutSquare β₁ β₂ α₁ α₂)
173 (hpo' : IsPushoutSquare β₁ β₂ α₁' α₂') :
174 G ≅ G' where
175 hom := pushoutMapOfIsPushout β₁ β₂ hpo hpo'
176 inv := pushoutMapOfIsPushout β₁ β₂ hpo' hpo
177 hom_inv_id := by
178 apply pushout_hom_ext hpo
179 · calc
180 α₁ ≫ pushoutMapOfIsPushout β₁ β₂ hpo hpo' ≫
181 pushoutMapOfIsPushout β₁ β₂ hpo' hpo =
182 α₁' ≫ pushoutMapOfIsPushout β₁ β₂ hpo' hpo := by
183 rw [← Category.assoc, pushoutMapOfIsPushout_left]
184 _ = α₁ := pushoutMapOfIsPushout_left β₁ β₂ hpo' hpo
185 · calc
186 α₂ ≫ pushoutMapOfIsPushout β₁ β₂ hpo hpo' ≫
187 pushoutMapOfIsPushout β₁ β₂ hpo' hpo =
188 α₂' ≫ pushoutMapOfIsPushout β₁ β₂ hpo' hpo := by
189 rw [← Category.assoc, pushoutMapOfIsPushout_right]
190 _ = α₂ := pushoutMapOfIsPushout_right β₁ β₂ hpo' hpo
191 inv_hom_id := by
192 apply pushout_hom_ext hpo'
193 · calc
194 α₁' ≫ pushoutMapOfIsPushout β₁ β₂ hpo' hpo ≫
195 pushoutMapOfIsPushout β₁ β₂ hpo hpo' =
196 α₁ ≫ pushoutMapOfIsPushout β₁ β₂ hpo hpo' := by
197 rw [← Category.assoc, pushoutMapOfIsPushout_left]
198 _ = α₁' := pushoutMapOfIsPushout_left β₁ β₂ hpo hpo'
199 · calc
200 α₂' ≫ pushoutMapOfIsPushout β₁ β₂ hpo' hpo ≫
201 pushoutMapOfIsPushout β₁ β₂ hpo hpo' =
202 α₂ ≫ pushoutMapOfIsPushout β₁ β₂ hpo hpo' := by
203 rw [← Category.assoc, pushoutMapOfIsPushout_right]
204 _ = α₂' := pushoutMapOfIsPushout_right β₁ β₂ hpo hpo'
206/-- The canonical pushout isomorphism respects the left structure map. -/
208 {α₁ : H₁ ⟶ G} {α₂ : H₂ ⟶ G}
209 {α₁' : H₁ ⟶ G'} {α₂' : H₂ ⟶ G'}
210 (β₁ : H ⟶ H₁) (β₂ : H ⟶ H₂)
211 (hpo : IsPushoutSquare β₁ β₂ α₁ α₂)
212 (hpo' : IsPushoutSquare β₁ β₂ α₁' α₂') :
213 α₁ ≫ (pushoutIsoOfIsPushout β₁ β₂ hpo hpo').hom = α₁' :=
214 pushoutMapOfIsPushout_left β₁ β₂ hpo hpo'
216/-- The canonical pushout isomorphism respects the right structure map. -/
218 {α₁ : H₁ ⟶ G} {α₂ : H₂ ⟶ G}
219 {α₁' : H₁ ⟶ G'} {α₂' : H₂ ⟶ G'}
220 (β₁ : H ⟶ H₁) (β₂ : H ⟶ H₂)
221 (hpo : IsPushoutSquare β₁ β₂ α₁ α₂)
222 (hpo' : IsPushoutSquare β₁ β₂ α₁' α₂') :
223 α₂ ≫ (pushoutIsoOfIsPushout β₁ β₂ hpo hpo').hom = α₂' :=
224 pushoutMapOfIsPushout_right β₁ β₂ hpo hpo'