Base approximations

In this file, we define base approximations, and what it means for a base approximation to (exactly) approximate some base permutation.

Main declarations

• ConNF.BaseApprox: The type of base approximations.
• ConNF.BaseApprox.Approximates, ConNF.BaseApprox.ExactlyApproximates: Propositions that indicate that a base approximation (exactly) approximates a given base permutation.

theorem ConNF.BaseApprox.ext : ∀ {inst : ConNF.Params} (x y : ConNF.BaseApprox), x.atomPerm = y.atomPerm → x.litterPerm = y.litterPerm → x = y

theorem ConNF.BaseApprox.ext_iff : ∀ {inst : ConNF.Params} (x y : ConNF.BaseApprox), x = y ↔ x.atomPerm = y.atomPerm ∧ x.litterPerm = y.litterPerm

structure ConNF.BaseApprox [ConNF.Params] : Type u

A base approximation consists of a partial permutation of atoms and a partial permutation of litters, in such a way that only a small amount of atoms in the domain intersect any given litter set.

• atomPerm : PartialPerm ConNF.Atom
• litterPerm : PartialPerm ConNF.Litter
• domain_small : ∀ (L : ConNF.Litter), ConNF.Small (ConNF.litterSet L ∩ self.atomPerm.domain)

theorem ConNF.BaseApprox.domain_small [ConNF.Params] (self : ConNF.BaseApprox) (L : ConNF.Litter) : ConNF.Small (ConNF.litterSet L ∩ self.atomPerm.domain)

instance ConNF.BaseApprox.instSMulAtom [ConNF.Params] : SMul ConNF.BaseApprox ConNF.Atom

Equations

• ConNF.BaseApprox.instSMulAtom = { smul := fun (π : ConNF.BaseApprox) => π.atomPerm.toFun }

instance ConNF.BaseApprox.instSMulLitter [ConNF.Params] : SMul ConNF.BaseApprox ConNF.Litter

Equations

• ConNF.BaseApprox.instSMulLitter = { smul := fun (π : ConNF.BaseApprox) => π.litterPerm.toFun }

theorem ConNF.BaseApprox.smul_atom_eq [ConNF.Params] (π : ConNF.BaseApprox) {a : ConNF.Atom} : π.atomPerm.toFun a = π • a

theorem ConNF.BaseApprox.smul_litter_eq [ConNF.Params] (π : ConNF.BaseApprox) {L : ConNF.Litter} : π.litterPerm.toFun L = π • L

@[simp]

theorem ConNF.BaseApprox.mk_smul_atom [ConNF.Params] {atomPerm : PartialPerm ConNF.Atom} {litterPerm : PartialPerm ConNF.Litter} {domain_small : ∀ (L : ConNF.Litter), ConNF.Small (ConNF.litterSet L ∩ atomPerm.domain)} {a : ConNF.Atom} : { atomPerm := atomPerm, litterPerm := litterPerm, domain_small := domain_small } • a = atomPerm.toFun a

@[simp]

theorem ConNF.BaseApprox.mk_smul_litter [ConNF.Params] {atomPerm : PartialPerm ConNF.Atom} {litterPerm : PartialPerm ConNF.Litter} {domain_small : ∀ (L : ConNF.Litter), ConNF.Small (ConNF.litterSet L ∩ atomPerm.domain)} {L : ConNF.Litter} : { atomPerm := atomPerm, litterPerm := litterPerm, domain_small := domain_small } • L = litterPerm.toFun L

theorem ConNF.BaseApprox.smul_eq_smul_atom [ConNF.Params] (π : ConNF.BaseApprox) {a₁ : ConNF.Atom} {a₂ : ConNF.Atom} (h₁ : a₁ ∈ π.atomPerm.domain) (h₂ : a₂ ∈ π.atomPerm.domain) : π • a₁ = π • a₂ ↔ a₁ = a₂

theorem ConNF.BaseApprox.smul_eq_smul_litter [ConNF.Params] (π : ConNF.BaseApprox) {L₁ : ConNF.Litter} {L₂ : ConNF.Litter} (h₁ : L₁ ∈ π.litterPerm.domain) (h₂ : L₂ ∈ π.litterPerm.domain) : π • L₁ = π • L₂ ↔ L₁ = L₂

def ConNF.BaseApprox.symm [ConNF.Params] (π : ConNF.BaseApprox) : ConNF.BaseApprox

Equations

• π.symm = { atomPerm := π.atomPerm.symm, litterPerm := π.litterPerm.symm, domain_small := ⋯ }

@[simp]

theorem ConNF.BaseApprox.symm_atomPerm [ConNF.Params] (π : ConNF.BaseApprox) : π.symm.atomPerm = π.atomPerm.symm

@[simp]

theorem ConNF.BaseApprox.symm_litterPerm [ConNF.Params] (π : ConNF.BaseApprox) : π.symm.litterPerm = π.litterPerm.symm

@[simp]

theorem ConNF.BaseApprox.left_inv_atom [ConNF.Params] (π : ConNF.BaseApprox) {a : ConNF.Atom} : a ∈ π.atomPerm.domain → π.symm • π • a = a

@[simp]

theorem ConNF.BaseApprox.left_inv_litter [ConNF.Params] (π : ConNF.BaseApprox) {L : ConNF.Litter} : L ∈ π.litterPerm.domain → π.symm • π • L = L

@[simp]

theorem ConNF.BaseApprox.right_inv_atom [ConNF.Params] (π : ConNF.BaseApprox) {a : ConNF.Atom} : a ∈ π.atomPerm.domain → π • π.symm • a = a

@[simp]

theorem ConNF.BaseApprox.right_inv_litter [ConNF.Params] (π : ConNF.BaseApprox) {L : ConNF.Litter} : L ∈ π.litterPerm.domain → π • π.symm • L = L

theorem ConNF.BaseApprox.symm_smul_atom_eq_iff [ConNF.Params] (π : ConNF.BaseApprox) {a : ConNF.Atom} {b : ConNF.Atom} : a ∈ π.atomPerm.domain → b ∈ π.atomPerm.domain → (π.symm • a = b ↔ a = π • b)

theorem ConNF.BaseApprox.symm_smul_litter_eq_iff [ConNF.Params] (π : ConNF.BaseApprox) {L₁ : ConNF.Litter} {L₂ : ConNF.Litter} : L₁ ∈ π.litterPerm.domain → L₂ ∈ π.litterPerm.domain → (π.symm • L₁ = L₂ ↔ L₁ = π • L₂)

theorem ConNF.BaseApprox.eq_symm_apply_atom [ConNF.Params] (π : ConNF.BaseApprox) {a₁ : ConNF.Atom} {a₂ : ConNF.Atom} : a₁ ∈ π.atomPerm.domain → a₂ ∈ π.atomPerm.domain → (a₁ = π.symm • a₂ ↔ π • a₁ = a₂)

theorem ConNF.BaseApprox.eq_symm_apply_litter [ConNF.Params] (π : ConNF.BaseApprox) {L₁ : ConNF.Litter} {L₂ : ConNF.Litter} : L₁ ∈ π.litterPerm.domain → L₂ ∈ π.litterPerm.domain → (L₁ = π.symm • L₂ ↔ π • L₁ = L₂)

theorem ConNF.BaseApprox.nearLitter_domain_small [ConNF.Params] (π : ConNF.BaseApprox) (N : ConNF.NearLitter) : ConNF.Small (↑N ∩ π.atomPerm.domain)

def ConNF.BaseApprox.largestSublitter [ConNF.Params] (π : ConNF.BaseApprox) (L : ConNF.Litter) : ConNF.Sublitter

Gives the largest sublitter of π on which π.atom_perm is not defined.

Equations

• π.largestSublitter L = { litter := L, carrier := ConNF.litterSet L \ π.atomPerm.domain, subset := ⋯, diff_small := ⋯ }

@[simp]

theorem ConNF.BaseApprox.largestSublitter_litter [ConNF.Params] (π : ConNF.BaseApprox) (L : ConNF.Litter) : (π.largestSublitter L).litter = L

@[simp]

theorem ConNF.BaseApprox.coe_largestSublitter [ConNF.Params] (π : ConNF.BaseApprox) (L : ConNF.Litter) : ↑(π.largestSublitter L) = ConNF.litterSet L \ π.atomPerm.domain

theorem ConNF.BaseApprox.mem_largestSublitter_of_not_mem_domain [ConNF.Params] (π : ConNF.BaseApprox) (a : ConNF.Atom) (h : a ∉ π.atomPerm.domain) : a ∈ π.largestSublitter a.1

theorem ConNF.BaseApprox.not_mem_domain_of_mem_largestSublitter [ConNF.Params] (π : ConNF.BaseApprox) {a : ConNF.Atom} {L : ConNF.Litter} (h : a ∈ π.largestSublitter L) : a ∉ π.atomPerm.domain

def ConNF.BasePerm.IsException [ConNF.Params] (π : ConNF.BasePerm) (a : ConNF.Atom) : Prop

Equations

• π.IsException a = (π • a ∉ ConNF.litterSet (π • a.1) ∨ π⁻¹ • a ∉ ConNF.litterSet (π⁻¹ • a.1))

theorem ConNF.BaseApprox.approximates_iff [ConNF.Params] (π₀ : ConNF.BaseApprox) (π : ConNF.BasePerm) : π₀.Approximates π ↔ (∀ a ∈ π₀.atomPerm.domain, π₀ • a = π • a) ∧ ∀ L ∈ π₀.litterPerm.domain, π₀ • L = π • L

structure ConNF.BaseApprox.Approximates [ConNF.Params] (π₀ : ConNF.BaseApprox) (π : ConNF.BasePerm) : Prop

A base approximation approximates a base permutation if they agree wherever they are both defined. Note that a base approximation does not define images of near-litters; we only require that the base permutation agrees with it for atoms and litters.

• map_atom : ∀ a ∈ π₀.atomPerm.domain, π₀ • a = π • a
• map_litter : ∀ L ∈ π₀.litterPerm.domain, π₀ • L = π • L

theorem ConNF.BaseApprox.Approximates.map_atom [ConNF.Params] {π₀ : ConNF.BaseApprox} {π : ConNF.BasePerm} (self : π₀.Approximates π) (a : ConNF.Atom) : a ∈ π₀.atomPerm.domain → π₀ • a = π • a

theorem ConNF.BaseApprox.Approximates.map_litter [ConNF.Params] {π₀ : ConNF.BaseApprox} {π : ConNF.BasePerm} (self : π₀.Approximates π) (L : ConNF.Litter) : L ∈ π₀.litterPerm.domain → π₀ • L = π • L

theorem ConNF.BaseApprox.Approximates.symm_map_atom [ConNF.Params] {π₀ : ConNF.BaseApprox} {π : ConNF.BasePerm} (hπ : π₀.Approximates π) (a : ConNF.Atom) (ha : a ∈ π₀.atomPerm.domain) : π₀.symm • a = π⁻¹ • a

theorem ConNF.BaseApprox.Approximates.symm_map_litter [ConNF.Params] {π₀ : ConNF.BaseApprox} {π : ConNF.BasePerm} (hπ : π₀.Approximates π) (L : ConNF.Litter) (hL : L ∈ π₀.litterPerm.domain) : π₀.symm • L = π⁻¹ • L

theorem ConNF.BaseApprox.exactlyApproximates_iff [ConNF.Params] (π₀ : ConNF.BaseApprox) (π : ConNF.BasePerm) : π₀.ExactlyApproximates π ↔ π₀.Approximates π ∧ ∀ (a : ConNF.Atom), π.IsException a → a ∈ π₀.atomPerm.domain

structure ConNF.BaseApprox.ExactlyApproximates [ConNF.Params] (π₀ : ConNF.BaseApprox) (π : ConNF.BasePerm) extends ConNF.BaseApprox.Approximates : Prop

A base approximation φ exactly approximates a base permutation π if they agree wherever they are both defined, and every exception of π is in the domain of φ. This allows us to precisely calculate images of near-litters under π.

• map_atom : ∀ a ∈ π₀.atomPerm.domain, π₀ • a = π • a
• map_litter : ∀ L ∈ π₀.litterPerm.domain, π₀ • L = π • L
• exception_mem : ∀ (a : ConNF.Atom), π.IsException a → a ∈ π₀.atomPerm.domain

theorem ConNF.BaseApprox.ExactlyApproximates.exception_mem [ConNF.Params] {π₀ : ConNF.BaseApprox} {π : ConNF.BasePerm} (self : π₀.ExactlyApproximates π) (a : ConNF.Atom) : π.IsException a → a ∈ π₀.atomPerm.domain

theorem ConNF.BaseApprox.ExactlyApproximates.of_isException [ConNF.Params] {π₀ : ConNF.BaseApprox} {π : ConNF.BasePerm} (hπ : π₀.ExactlyApproximates π) (a : ConNF.Atom) (ha : a.1 ∈ π₀.litterPerm.domain) : π.IsException a → π₀ • a ∉ ConNF.litterSet (π₀ • a.1) ∨ π₀.symm • a ∉ ConNF.litterSet (π₀.symm • a.1)

theorem ConNF.BaseApprox.ExactlyApproximates.mem_litterSet [ConNF.Params] {π₀ : ConNF.BaseApprox} {π : ConNF.BasePerm} (hπ : π₀.ExactlyApproximates π) (a : ConNF.Atom) (ha : a ∉ π₀.atomPerm.domain) : π • a ∈ ConNF.litterSet (π • a.1)

theorem ConNF.BaseApprox.ExactlyApproximates.mem_litterSet_inv [ConNF.Params] {π₀ : ConNF.BaseApprox} {π : ConNF.BasePerm} (hπ : π₀.ExactlyApproximates π) (a : ConNF.Atom) (ha : a ∉ π₀.atomPerm.domain) : π⁻¹ • a ∈ ConNF.litterSet (π⁻¹ • a.1)

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

A base approximation is said to be A-free if all of the litters in its domain are A-flexible.

Equations

• π.Free A = ∀ L ∈ π.litterPerm.domain, ConNF.Flexible A L