def
definition
compAutomorphism
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.RecogGeom.Symmetry on GitHub at line 180.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
177 right_inv := fun _ => rfl
178
179/-- Composition of automorphisms -/
180def compAutomorphism (T₁ T₂ : RecognitionAutomorphism r) : RecognitionAutomorphism r where
181 toFun := T₁.toFun ∘ T₂.toFun
182 preserves_event := fun c => by
183 simp only [Function.comp_apply]
184 rw [T₁.preserves_event, T₂.preserves_event]
185 invFun := T₂.invFun ∘ T₁.invFun
186 left_inv := fun c => by
187 simp only [Function.comp_apply]
188 -- Goal: T₂.invFun (T₁.invFun (T₁.toFun (T₂.toFun c))) = c
189 have h1 : T₁.invFun (T₁.toFun (T₂.toFun c)) = T₂.toFun c := T₁.left_inv _
190 rw [h1, T₂.left_inv]
191 right_inv := fun c => by
192 simp only [Function.comp_apply]
193 -- Goal: T₁.toFun (T₂.toFun (T₂.invFun (T₁.invFun c))) = c
194 have h1 : T₂.toFun (T₂.invFun (T₁.invFun c)) = T₁.invFun c := T₂.right_inv _
195 rw [h1, T₁.right_inv]
196
197/-! ## Algebraic Properties of Automorphisms -/
198
199/-- Composition of automorphisms is associative (on toFun) -/
200theorem compAutomorphism_assoc_toFun (T₁ T₂ T₃ : RecognitionAutomorphism r) :
201 (compAutomorphism (compAutomorphism T₁ T₂) T₃).toFun =
202 (compAutomorphism T₁ (compAutomorphism T₂ T₃)).toFun := by
203 simp only [compAutomorphism, Function.comp_assoc]
204
205/-- Identity is left neutral for automorphisms (on toFun) -/
206theorem idAutomorphism_comp_left_toFun (T : RecognitionAutomorphism r) :
207 (compAutomorphism idAutomorphism T).toFun = T.toFun := by
208 simp only [compAutomorphism, idAutomorphism, Function.id_comp]
209
210/-- Identity is right neutral for automorphisms (on toFun) -/