structure
definition
RecognitionAutomorphism
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.RecogGeom.Symmetry on GitHub at line 148.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
of -
of -
T -
T -
of -
of -
identity -
is -
of -
of -
is -
E -
of -
of -
is -
T -
T -
of -
of -
inv -
is -
RecognitionPreservingMap -
inv -
identity
used by
-
compAutomorphism -
compAutomorphism_assoc_toFun -
compAutomorphism_inv_left_eq_id -
compAutomorphism_inv_left_toFun -
compAutomorphism_inv_right_eq_id -
compAutomorphism_inv_right_toFun -
GaugeEquivalent -
gaugeEquivalent_symm -
idAutomorphism -
idAutomorphism_comp_left_toFun -
idAutomorphism_comp_right_toFun -
symmetry_status
formal source
145/-! ## Bijective Symmetries (Automorphisms) -/
146
147/-- A bijective recognition-preserving map (automorphism) -/
148structure RecognitionAutomorphism (r : Recognizer C E) extends RecognitionPreservingMap r where
149 /-- The inverse function -/
150 invFun : C → C
151 /-- Left inverse property -/
152 left_inv : ∀ c, invFun (toFun c) = c
153 /-- Right inverse property -/
154 right_inv : ∀ c, toFun (invFun c) = c
155
156/-- The inverse of an automorphism preserves events -/
157theorem RecognitionAutomorphism.inv_preserves_event (T : RecognitionAutomorphism r) (c : C) :
158 r.R (T.invFun c) = r.R c := by
159 have h := T.preserves_event (T.invFun c)
160 rw [T.right_inv] at h
161 exact h.symm
162
163/-- The inverse of an automorphism is an automorphism -/
164def RecognitionAutomorphism.inv (T : RecognitionAutomorphism r) : RecognitionAutomorphism r where
165 toFun := T.invFun
166 preserves_event := T.inv_preserves_event
167 invFun := T.toFun
168 left_inv := T.right_inv
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