`idAutomorphism_comp_left_toFun`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.RecogGeom.Symmetry on GitHub at line 206.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 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) -/
 211theorem idAutomorphism_comp_right_toFun (T : RecognitionAutomorphism r) :
 212    (compAutomorphism T idAutomorphism).toFun = T.toFun := by
 213  simp only [compAutomorphism, idAutomorphism, Function.comp_id]
 214
 215/-- Right inverse property (on toFun) -/
 216theorem compAutomorphism_inv_right_toFun (T : RecognitionAutomorphism r) (c : C) :
 217    (compAutomorphism T T.inv).toFun c = c := by
 218  simp only [compAutomorphism, RecognitionAutomorphism.inv, Function.comp_apply]
 219  exact T.right_inv c
 220
 221/-- Left inverse property (on toFun) -/
 222theorem compAutomorphism_inv_left_toFun (T : RecognitionAutomorphism r) (c : C) :
 223    (compAutomorphism T.inv T).toFun c = c := by
 224  simp only [compAutomorphism, RecognitionAutomorphism.inv, Function.comp_apply]
 225  exact T.left_inv c
 226
 227/-- The composition T ∘ T⁻¹ acts as identity -/
 228theorem compAutomorphism_inv_right_eq_id (T : RecognitionAutomorphism r) :
 229    (compAutomorphism T T.inv).toFun = id := by
 230  ext c
 231  exact compAutomorphism_inv_right_toFun T c
 232
 233/-- The composition T⁻¹ ∘ T acts as identity -/
 234theorem compAutomorphism_inv_left_eq_id (T : RecognitionAutomorphism r) :
 235    (compAutomorphism T.inv T).toFun = id := by
 236  ext c

papers checked against this theorem

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