Twisting sets

In this file, we define the notion of a designated support for a t-set.

Main declarations

• ConNF.TSet.designatedSupport: The designated support for a t-set.

def ConNF.TSet.orbitRel [ConNF.Params] {α : ConNF.TypeIndex} [ConNF.ModelData α] : Rel (ConNF.TSet α) (ConNF.TSet α)

Equations

• ConNF.TSet.orbitRel x y = ∃ (ρ : ConNF.AllPerm α), ρ • x = y

theorem ConNF.TSet.orbitRel_isEquivalence [ConNF.Params] {α : ConNF.TypeIndex} [ConNF.ModelData α] : Equivalence ConNF.TSet.orbitRel

instance ConNF.TSet.setoid [ConNF.Params] (α : ConNF.TypeIndex) [ConNF.ModelData α] : Setoid (ConNF.TSet α)

Equations

• ConNF.TSet.setoid α = { r := ConNF.TSet.orbitRel, iseqv := ⋯ }

def ConNF.TSetOrbit [ConNF.Params] (α : ConNF.TypeIndex) [ConNF.ModelData α] : Type u

Equations

• ConNF.TSetOrbit α = Quotient (ConNF.TSet.setoid α)

def ConNF.TSet.orbit [ConNF.Params] {α : ConNF.TypeIndex} [ConNF.ModelData α] (x : ConNF.TSet α) : ConNF.TSetOrbit α

Equations

• ConNF.TSet.orbit x = ⟦x⟧

theorem ConNF.TSetOrbit.exists_tSet [ConNF.Params] {α : ConNF.TypeIndex} [ConNF.ModelData α] (o : ConNF.TSetOrbit α) : ∃ (x : ConNF.TSet α), ConNF.TSet.orbit x = o

theorem ConNF.TSet.orbit_eq_iff [ConNF.Params] {α : ConNF.TypeIndex} [ConNF.ModelData α] {x y : ConNF.TSet α} : ConNF.TSet.orbit x = ConNF.TSet.orbit y ↔ ∃ (ρ : ConNF.AllPerm α), ρ • x = y

@[simp]

theorem ConNF.TSet.smul_orbit [ConNF.Params] {α : ConNF.TypeIndex} [ConNF.ModelData α] {x : ConNF.TSet α} {ρ : ConNF.AllPerm α} : ConNF.TSet.orbit (ρ • x) = ConNF.TSet.orbit x

def ConNF.TSetOrbit.repr [ConNF.Params] {α : ConNF.TypeIndex} [ConNF.ModelData α] (o : ConNF.TSetOrbit α) : ConNF.TSet α

Equations

• o.repr = ⋯.choose

@[simp]

theorem ConNF.TSetOrbit.repr_orbit [ConNF.Params] {α : ConNF.TypeIndex} [ConNF.ModelData α] (o : ConNF.TSetOrbit α) : ConNF.TSet.orbit o.repr = o

def ConNF.TSetOrbit.repr_support [ConNF.Params] {α : ConNF.TypeIndex} [ConNF.ModelData α] (o : ConNF.TSetOrbit α) : ConNF.Support α

Equations

• o.repr_support = ⋯.choose

theorem ConNF.TSetOrbit.repr_support_spec [ConNF.Params] {α : ConNF.TypeIndex} [ConNF.ModelData α] (o : ConNF.TSetOrbit α) : o.repr_support.Supports o.repr

theorem ConNF.TSet.exists_twist [ConNF.Params] {α : ConNF.TypeIndex} [ConNF.ModelData α] (x : ConNF.TSet α) : ∃ (ρ : ConNF.AllPerm α), ρ • (ConNF.TSet.orbit x).repr = x

def ConNF.twist [ConNF.Params] {α : ConNF.TypeIndex} [ConNF.ModelData α] (x : ConNF.TSet α) : ConNF.AllPerm α

Equations

• ConNF.twist x = ⋯.choose

theorem ConNF.twist_spec [ConNF.Params] {α : ConNF.TypeIndex} [ConNF.ModelData α] (x : ConNF.TSet α) : ConNF.twist x • (ConNF.TSet.orbit x).repr = x

def ConNF.designatedSupport [ConNF.Params] {α : ConNF.TypeIndex} [ConNF.ModelData α] (x : ConNF.TSet α) : ConNF.Support α

Equations

• ConNF.designatedSupport x = (ConNF.twist x)ᵁ • (ConNF.TSet.orbit x).repr_support

theorem ConNF.designatedSupport_supports [ConNF.Params] {α : ConNF.TypeIndex} [ConNF.ModelData α] (x : ConNF.TSet α) : (ConNF.designatedSupport x).Supports x