Induced action: Flexible litters

In this file, we describe the induced action of an approximation on flexible litters.

Main declarations

• ConNF.BaseApprox.flexibleCompletion: Augments the litter permutation of a base approximation so that it is defined on all flexible litters.

def ConNF.BaseApprox.idOnFlexible [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.TypeIndex} (π : ConNF.BaseApprox) (A : ConNF.ExtendedIndex β) : PartialPerm ConNF.Litter

Equations

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

theorem ConNF.BaseApprox.idOnFlexible_domain [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.TypeIndex} (π : ConNF.BaseApprox) (A : ConNF.ExtendedIndex β) : (π.idOnFlexible A).domain = {L : ConNF.Litter | ConNF.Flexible A L} \ π.litterPerm.domain

theorem ConNF.BaseApprox.idOnFlexible_domain_disjoint [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.TypeIndex} (π : ConNF.BaseApprox) (A : ConNF.ExtendedIndex β) : Disjoint π.litterPerm.domain (π.idOnFlexible A).domain

noncomputable def ConNF.BaseApprox.flexibleCompletionLitterPerm [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.TypeIndex} (π : ConNF.BaseApprox) (A : ConNF.ExtendedIndex β) : PartialPerm ConNF.Litter

Equations

• π.flexibleCompletionLitterPerm A = π.litterPerm.piecewise (π.idOnFlexible A) ⋯

theorem ConNF.BaseApprox.flexibleCompletionLitterPerm_domain [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.TypeIndex} (π : ConNF.BaseApprox) (A : ConNF.ExtendedIndex β) : (π.flexibleCompletionLitterPerm A).domain = π.litterPerm.domain ∪ {L : ConNF.Litter | ConNF.Flexible A L}

noncomputable def ConNF.BaseApprox.flexibleCompletion [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.TypeIndex} (π : ConNF.BaseApprox) (A : ConNF.ExtendedIndex β) : ConNF.BaseApprox

Equations

• π.flexibleCompletion A = { atomPerm := π.atomPerm, litterPerm := π.flexibleCompletionLitterPerm A, domain_small := ⋯ }

theorem ConNF.BaseApprox.flexibleCompletion_litterPerm_domain [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.TypeIndex} (π : ConNF.BaseApprox) (A : ConNF.ExtendedIndex β) : (π.flexibleCompletion A).litterPerm.domain = π.litterPerm.domain ∪ {L : ConNF.Litter | ConNF.Flexible A L}

theorem ConNF.BaseApprox.flexibleCompletion_litterPerm_domain_free [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.TypeIndex} (π : ConNF.BaseApprox) (A : ConNF.ExtendedIndex β) (hπ : π.Free A) : (π.flexibleCompletion A).litterPerm.domain = {L : ConNF.Litter | ConNF.Flexible A L}

theorem ConNF.BaseApprox.flexibleCompletion_smul_eq [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.TypeIndex} (π : ConNF.BaseApprox) (A : ConNF.ExtendedIndex β) (L : ConNF.Litter) : π.flexibleCompletion A • L = (π.flexibleCompletionLitterPerm A).toFun L

theorem ConNF.BaseApprox.flexibleCompletion_smul_of_mem_domain [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.TypeIndex} (π : ConNF.BaseApprox) (A : ConNF.ExtendedIndex β) (L : ConNF.Litter) (hL : L ∈ π.litterPerm.domain) : π.flexibleCompletion A • L = π.litterPerm.toFun L

theorem ConNF.BaseApprox.flexibleCompletion_smul_flexible [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.TypeIndex} (π : ConNF.BaseApprox) (A : ConNF.ExtendedIndex β) (hπ : π.Free A) (L : ConNF.Litter) (hL : ConNF.Flexible A L) : ConNF.Flexible A (π.flexibleCompletion A • L)

theorem ConNF.BaseApprox.flexibleCompletion_symm_smul_flexible [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.TypeIndex} (π : ConNF.BaseApprox) (A : ConNF.ExtendedIndex β) (hπ : π.Free A) (L : ConNF.Litter) (hL : ConNF.Flexible A L) : ConNF.Flexible A ((π.flexibleCompletion A).symm • L)