Automorphism Group of the Turing Degrees

This file sets up the automorphism group of the Turing degrees as the group of order isomorphisms of TuringDegree.

@[reducible, inline]

abbrev Computability.OrderAut (α : Type u_1) [LE α] : Type u_1

The order automorphisms of a type α, namely the order isomorphisms α ≃o α.

Equations

• Computability.OrderAut α = (α ≃o α)

@[implicit_reducible]

instance Computability.OrderAutGroup (α : Type) [LE α] : Group (OrderAut α)

The group structure on the order automorphisms of α.

Equations

• One or more equations did not get rendered due to their size.

def Computability.TuringDegree.automorphismGroup : Type

The automorphism group of the Turing degrees.

Equations

• Computability.TuringDegree.automorphismGroup = Computability.OrderAut Computability.TuringDegree

@[implicit_reducible]

instance Computability.TuringDegree.automorphismGroup.isGroup : Group automorphismGroup

Equations

• Computability.TuringDegree.automorphismGroup.isGroup = Computability.OrderAutGroup Computability.TuringDegree

@[implicit_reducible]

instance Computability.TuringDegree.automorphismGroup.existsAut : Inhabited automorphismGroup

Equations

• Computability.TuringDegree.automorphismGroup.existsAut = { default := OrderIso.refl Computability.TuringDegree }