theorem
proved
compAutomorphism_inv_left_toFun
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 222.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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
247/-- Gauge equivalence implies indistinguishability -/
248theorem gauge_implies_indistinguishable {c₁ c₂ : C}
249 (h : GaugeEquivalent r c₁ c₂) : Indistinguishable r c₁ c₂ := by
250 obtain ⟨T, hT⟩ := h
251 rw [← hT, Indistinguishable, T.preserves_event]
252