Documentation

ConNF.Base.BasePerm

Base permutations #

In this file, we define the group of base permutations, and their actions on atoms, litters, and near-litters.

Main declarations #

source
structure ConNF.BasePerm [ConNF.Params] :
Type u
  • atoms : Equiv.Perm ConNF.Atom
  • litters : Equiv.Perm ConNF.Litter
  • apply_near_apply : ∀ (s : Set ConNF.Atom) (L : ConNF.Litter), s ~ Lᴬ → ⇑self.atoms '' s ~ (self.litters L)ᴬ
Instances For
    source
    instance ConNF.BasePerm.instSuperAPermAtom [ConNF.Params] :
    ConNF.SuperA ConNF.BasePerm (Equiv.Perm ConNF.Atom)
    Equations
    • ConNF.BasePerm.instSuperAPermAtom = { superA := ConNF.BasePerm.atoms }
    source
    instance ConNF.BasePerm.instSuperLPermLitter [ConNF.Params] :
    ConNF.SuperL ConNF.BasePerm (Equiv.Perm ConNF.Litter)
    Equations
    • ConNF.BasePerm.instSuperLPermLitter = { superL := ConNF.BasePerm.litters }
    source
    instance ConNF.BasePerm.instSMulAtom [ConNF.Params] :
    SMul ConNF.BasePerm ConNF.Atom
    Equations
    • ConNF.BasePerm.instSMulAtom = { smul := fun (π : ConNF.BasePerm) (a : ConNF.Atom) => πᴬ a }
    source
    instance ConNF.BasePerm.instSMulLitter [ConNF.Params] :
    SMul ConNF.BasePerm ConNF.Litter
    Equations
    • ConNF.BasePerm.instSMulLitter = { smul := fun (π : ConNF.BasePerm) (L : ConNF.Litter) => πᴸ L }
    source
    theorem ConNF.BasePerm.smul_near_smul [ConNF.Params] (π : ConNF.BasePerm) (s : Set ConNF.Atom) (L : ConNF.Litter) :
    s ~ Lᴬ → π • s ~ (π • L)ᴬ
    source
    instance ConNF.BasePerm.instSMulNearLitter [ConNF.Params] :
    SMul ConNF.BasePerm ConNF.NearLitter
    Equations
    • ConNF.BasePerm.instSMulNearLitter = { smul := fun (π : ConNF.BasePerm) (N : ConNF.NearLitter) => { litter := π • Nᴸ, atoms := π • Nᴬ, atoms_near_litter' := ⋯ } }
    source
    theorem ConNF.BasePerm.smul_atom_def [ConNF.Params] (π : ConNF.BasePerm) (a : ConNF.Atom) :
    π • a = πᴬ a
    source
    theorem ConNF.BasePerm.smul_litter_def [ConNF.Params] (π : ConNF.BasePerm) (L : ConNF.Litter) :
    π • L = πᴸ L
    source
    @[simp]
    theorem ConNF.BasePerm.smul_nearLitter_atoms [ConNF.Params] (π : ConNF.BasePerm) (N : ConNF.NearLitter) :
    (π • N)ᴬ = π • Nᴬ
    source
    @[simp]
    theorem ConNF.BasePerm.smul_nearLitter_litter [ConNF.Params] (π : ConNF.BasePerm) (N : ConNF.NearLitter) :
    (π • N)ᴸ = π • Nᴸ
    source
    theorem ConNF.BasePerm.ext [ConNF.Params] {π₁ π₂ : ConNF.BasePerm} (h : ∀ (a : ConNF.Atom), π₁ • a = π₂ • a) :
    π₁ = π₂
    source
    instance ConNF.BasePerm.instOne [ConNF.Params] :
    One ConNF.BasePerm
    Equations
    • ConNF.BasePerm.instOne = { one := { atoms := 1, litters := 1, apply_near_apply := ⋯ } }
    source
    @[simp]
    theorem ConNF.BasePerm.one_atom [ConNF.Params] :
    1ᴬ = 1
    source
    @[simp]
    theorem ConNF.BasePerm.one_litter [ConNF.Params] :
    1ᴸ = 1
    source
    instance ConNF.BasePerm.instMul [ConNF.Params] :
    Mul ConNF.BasePerm
    Equations
    • ConNF.BasePerm.instMul = { mul := fun (π₁ π₂ : ConNF.BasePerm) => { atoms := π₁ᴬ * π₂ᴬ, litters := π₁ᴸ * π₂ᴸ, apply_near_apply := ⋯ } }
    source
    @[simp]
    theorem ConNF.BasePerm.mul_atom [ConNF.Params] (π₁ π₂ : ConNF.BasePerm) :
    (π₁ * π₂)ᴬ = π₁ᴬ * π₂ᴬ
    source
    @[simp]
    theorem ConNF.BasePerm.mul_litter [ConNF.Params] (π₁ π₂ : ConNF.BasePerm) :
    (π₁ * π₂)ᴸ = π₁ᴸ * π₂ᴸ
    source
    theorem ConNF.BasePerm.inv_smul_near_inv_smul [ConNF.Params] (π : ConNF.BasePerm) (s : Set ConNF.Atom) (L : ConNF.Litter) :
    s ~ Lᴬ → πᴬ⁻¹ • s ~ (πᴸ⁻¹ • L)ᴬ
    source
    instance ConNF.BasePerm.instInv [ConNF.Params] :
    Inv ConNF.BasePerm
    Equations
    • ConNF.BasePerm.instInv = { inv := fun (π : ConNF.BasePerm) => { atoms := πᴬ⁻¹, litters := πᴸ⁻¹, apply_near_apply := ⋯ } }
    source
    @[simp]
    theorem ConNF.BasePerm.inv_atom [ConNF.Params] (π : ConNF.BasePerm) :
    π⁻¹ᴬ = πᴬ⁻¹
    source
    @[simp]
    theorem ConNF.BasePerm.inv_litter [ConNF.Params] (π : ConNF.BasePerm) :
    π⁻¹ᴸ = πᴸ⁻¹
    source
    instance ConNF.BasePerm.instGroup [ConNF.Params] :
    Group ConNF.BasePerm
    Equations
    source
    instance ConNF.BasePerm.instMulActionAtom [ConNF.Params] :
    MulAction ConNF.BasePerm ConNF.Atom
    Equations
    source
    instance ConNF.BasePerm.instMulActionLitter [ConNF.Params] :
    MulAction ConNF.BasePerm ConNF.Litter
    Equations
    source
    instance ConNF.BasePerm.instMulActionNearLitter [ConNF.Params] :
    MulAction ConNF.BasePerm ConNF.NearLitter
    Equations
    source
    @[simp]
    theorem ConNF.BasePerm.smul_interference [ConNF.Params] (π : ConNF.BasePerm) (N₁ N₂ : ConNF.NearLitter) :
    π • ConNF.interference N₁ N₂ = ConNF.interference (π • N₁) (π • N₂)