compAutomorphism_inv_right_toFun

formal source

 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
 237  exact compAutomorphism_inv_left_toFun T c
 238
 239/-! ## Physical Interpretation: Gauge Equivalence -/
 240
 241/-- Two configurations are **gauge equivalent** if there exists a symmetry
 242    mapping one to the other. This captures the physical notion that
 243    gauge-related configurations are "the same" physically. -/
 244def GaugeEquivalent (r : Recognizer C E) (c₁ c₂ : C) : Prop :=
 245  ∃ T : RecognitionAutomorphism r, T.toFun c₁ = c₂
 246