structure System.Symmetry {S T : Type u} (sys : System S T) : Type u

• ft : T ≃ T
• fs : S ≃ S

theorem System.Symmetry.ext {S T : Type u} {sys : System S T} {x y : sys.Symmetry} (ft : x.ft = y.ft) (fs : x.fs = y.fs) : x = y

theorem System.Symmetry.ext_iff {S T : Type u} {sys : System S T} {x y : sys.Symmetry} : x = y ↔ x.ft = y.ft ∧ x.fs = y.fs

def System.Symmetry.ft' {S T : Type u} {sys : System S T} (sym : sys.Symmetry) : T ≃ T

Equations

• sym.ft' = sym.ft.symm

def System.Symmetry.fs' {S T : Type u} {sys : System S T} (sym : sys.Symmetry) : S ≃ S

Equations

• sym.fs' = sym.fs.symm

class System.Symmetry.WF {S T : Type u} {sys : System S T} (sym : sys.Symmetry) : Prop

• initial_fs_iff {s : S} : sys.Initial (sym.fs s) ↔ sys.Initial s
• tr_eq {s : S} {t : T} : sys.tr s t = Option.map (⇑sym.fs') (sys.tr (sym.fs s) (sym.ft t))

def System.Symmetry.one {S T : Type u} {sys : System S T} : sys.Symmetry

Equations

• System.Symmetry.one = { ft := Equiv.refl T, fs := Equiv.refl S }

@[instance_reducible]

instance System.Symmetry.instOne {S T : Type u} {sys : System S T} : One sys.Symmetry

Equations

• System.Symmetry.instOne = { one := System.Symmetry.one }

theorem System.Symmetry.one_def {S T : Type u} {sys : System S T} : 1 = one

@[instance_reducible]

instance System.Symmetry.instInhabited {S T : Type u} {sys : System S T} : Inhabited sys.Symmetry

Equations

• System.Symmetry.instInhabited = { default := 1 }

theorem System.Symmetry.default_def {S T : Type u} {sys : System S T} : default = 1

def System.Symmetry.simFn {S T : Type u} {sys : System S T} (sym : sys.Symmetry) (f : S → T) (s : S) : T

Equations

• sym.simFn f s = sym.ft (f (sym.fs' s))

def System.Symmetry.simFn' {S T : Type u} {sys : System S T} (sym : sys.Symmetry) (f : S → T) (s : S) : T

Equations

• sym.simFn' f s = sym.ft' (f (sym.fs s))

def System.Symmetry.inv {S T : Type u} {sys : System S T} (sym : sys.Symmetry) : sys.Symmetry

Equations

• sym.inv = { ft := sym.ft', fs := sym.fs' }

@[instance_reducible]

instance System.Symmetry.instInv {S T : Type u} {sys : System S T} : Inv sys.Symmetry

Equations

• System.Symmetry.instInv = { inv := System.Symmetry.inv }

theorem System.Symmetry.inv_def {S T : Type u} {sys : System S T} {sym : sys.Symmetry} : sym⁻¹ = sym.inv

def System.Symmetry.mul {S T : Type u} {sys : System S T} (sym₁ sym₂ : sys.Symmetry) : sys.Symmetry

Equations

• sym₁.mul sym₂ = { ft := sym₁.ft.comp sym₂.ft, fs := sym₁.fs.comp sym₂.fs }

@[instance_reducible]

instance System.Symmetry.instMul {S T : Type u} {sys : System S T} : Mul sys.Symmetry

Equations

• System.Symmetry.instMul = { mul := System.Symmetry.mul }

theorem System.Symmetry.mul_def {S T : Type u} {sys : System S T} {sym₁ sym₂ : sys.Symmetry} : sym₁ * sym₂ = sym₁.mul sym₂

def System.Symmetry.div {S T : Type u} {sys : System S T} (sym₁ sym₂ : sys.Symmetry) : sys.Symmetry

Equations

• sym₁.div sym₂ = sym₁ * sym₂⁻¹

@[instance_reducible]

instance System.Symmetry.instDiv {S T : Type u} {sys : System S T} : Div sys.Symmetry

Equations

• System.Symmetry.instDiv = { div := System.Symmetry.div }

theorem System.Symmetry.div_def {S T : Type u} {sys : System S T} {sym₁ sym₂ : sys.Symmetry} : sym₁ / sym₂ = sym₁ * sym₂⁻¹

def System.Symmetry.npow {S T : Type u} {sys : System S T} (n : ℕ) (sym : sys.Symmetry) : sys.Symmetry

Equations

• System.Symmetry.npow n sym = (fun (x : sys.Symmetry) => x * sym)^[n] 1

def System.Symmetry.zpow {S T : Type u} {sys : System S T} (z : ℤ) (sym : sys.Symmetry) : sys.Symmetry

Equations

• System.Symmetry.zpow (Int.ofNat n) sym = System.Symmetry.npow n sym
• System.Symmetry.zpow (Int.negSucc n) sym = System.Symmetry.npow (n + 1) sym⁻¹

class System.Symmetry.SelfInverse {S T : Type u} {sys : System S T} (sym : sys.Symmetry) extends sym.WF : Prop

• initial_fs_iff {s : S} : sys.Initial (sym.fs s) ↔ sys.Initial s
• tr_eq {s : S} {t : T} : sys.tr s t = Option.map (⇑sym.fs') (sys.tr (sym.fs s) (sym.ft t))
• inv_eq_self : sym⁻¹ = sym