OctaveEquiv

formal source

  85
  86/-- Two octaves are equivalent if there exist mutually inverse morphisms
  87    that both preserve strain exactly (isometric in both directions). -/
  88structure OctaveEquiv (O₁ O₂ : Octave) where
  89  /-- Forward morphism. -/
  90  toFun : OctaveMorphism O₁ O₂
  91  /-- Backward morphism. -/
  92  invFun : OctaveMorphism O₂ O₁
  93  /-- Strain is preserved exactly (forward isometry). -/
  94  strain_eq : ∀ x, O₂.strain.J (toFun.map x) = O₁.strain.J x
  95  /-- Strain is preserved exactly (inverse isometry). -/
  96  strain_eq_inv : ∀ y, O₁.strain.J (invFun.map y) = O₂.strain.J y
  97
  98namespace OctaveEquiv
  99
 100/-- Reflexivity. -/
 101def refl (O : Octave) : OctaveEquiv O O where
 102  toFun := OctaveMorphism.id O
 103  invFun := OctaveMorphism.id O
 104  strain_eq := fun _ => rfl
 105  strain_eq_inv := fun _ => rfl
 106
 107/-- Symmetry. -/
 108def symm {O₁ O₂ : Octave} (e : OctaveEquiv O₁ O₂) : OctaveEquiv O₂ O₁ where
 109  toFun := e.invFun
 110  invFun := e.toFun
 111  strain_eq := e.strain_eq_inv
 112  strain_eq_inv := e.strain_eq
 113
 114end OctaveEquiv
 115
 116/-- The "octave index" in Z (integer rung number).
 117    This is just a type alias; the physical interpretation is in Hypotheses. -/
 118abbrev OctaveRung := ℤ