`idAutomorphism`

definition

show as: view math explainer →

module: IndisputableMonolith.RecogGeom.Symmetry
domain: RecogGeom
line: 172 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.RecogGeom.Symmetry on GitHub at line 172.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 169  right_inv := T.left_inv
 170
 171/-- The identity automorphism -/
 172def idAutomorphism : RecognitionAutomorphism r where
 173  toFun := id
 174  preserves_event := fun _ => rfl
 175  invFun := id
 176  left_inv := fun _ => rfl
 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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.