Hypotheses for constructing the fuzz map

This file contains the inductive hypotheses required for constructing the fuzz map. Even though not everything defined here is strictly necessary for this construction, we bundle it here for more convenient use later.

Main declarations

• ConNF.ModelData: Data about the model elements at level α, called t-sets.
• ConNF.Tangle: A t-set together with a support for it.
• ConNF.PositionedTangles: A function that gives each type α tangle a unique position ν : μ.
• ConNF.TypedObjects: Allows us to encode near-litters as type α t-sets.
• ConNF.BasePositions: Almost arbitrarily chosen position functions for atoms and near-litters.
• ConNF.PositionedObjects: Hypotheses on the positions of typed objects.

class ConNF.ModelData [ConNF.Params] (α : ConNF.TypeIndex) : Type (u + 1)

Data about the model elements at level α. This class asserts the existence of a type of model elements at level α called t-sets, and a group of allowable permutations at level α that act on the type α t-sets. We also stipulate that each t-set has a support. There is a natural embedding of t-sets into structural sets.

• TSet : Type u

  The type of model elements that we assume were constructed at stage α. Later in the recursion, we will construct this type explicitly, but for now, we will just assume that it exists.

• Allowable : Type u

  The type of allowable permutations that we assume exists on α-tangles.

• allowableGroup : Group (ConNF.Allowable α)
• allowableToStructPerm : ConNF.Allowable α →* ConNF.StructPerm α

  An embedding from allowable permutations to structural permutations.

• allowableToStructPerm_injective : Function.Injective ⇑ConNF.ModelData.allowableToStructPerm
• allowableAction : MulAction (ConNF.Allowable α) (ConNF.TSet α)
• has_support : ∀ (t : ConNF.TSet α), ∃ (S : ConNF.Support α), MulAction.Supports (ConNF.Allowable α) (ConNF.Enumeration.carrier S) t
• toStructSet : ConNF.TSet α ↪ ConNF.StructSet α

  The embedding that converts a t-sets into its underlying structural set.

• toStructSet_smul : ∀ (ρ : ConNF.Allowable α) (t : ConNF.TSet α), ConNF.toStructSet (ρ • t) = ρ • ConNF.toStructSet t

theorem ConNF.ModelData.allowableToStructPerm_injective [ConNF.Params] {α : ConNF.TypeIndex} [self : ConNF.ModelData α] : Function.Injective ⇑ConNF.ModelData.allowableToStructPerm

theorem ConNF.ModelData.has_support [ConNF.Params] {α : ConNF.TypeIndex} [self : ConNF.ModelData α] (t : ConNF.TSet α) : ∃ (S : ConNF.Support α), MulAction.Supports (ConNF.Allowable α) (ConNF.Enumeration.carrier S) t

theorem ConNF.ModelData.toStructSet_smul [ConNF.Params] {α : ConNF.TypeIndex} [self : ConNF.ModelData α] (ρ : ConNF.Allowable α) (t : ConNF.TSet α) : ConNF.toStructSet (ρ • t) = ρ • ConNF.toStructSet t

def ConNF.Allowable.toStructPerm [ConNF.Params] {α : ConNF.TypeIndex} [ConNF.ModelData α] : ConNF.Allowable α →* ConNF.StructPerm α

Allowable permutations can be considered a subtype of structural permutations. This map can be thought of as an inclusion that preserves the group structure.

Equations

• ConNF.Allowable.toStructPerm = ConNF.ModelData.allowableToStructPerm

theorem ConNF.Allowable.toStructPerm_injective [ConNF.Params] (α : ConNF.TypeIndex) [ConNF.ModelData α] : Function.Injective ⇑ConNF.Allowable.toStructPerm

instance ConNF.Allowable.instMulActionAllowable [ConNF.Params] {α : ConNF.TypeIndex} [ConNF.ModelData α] {X : Type u_1} [MulAction (ConNF.StructPerm α) X] : MulAction (ConNF.Allowable α) X

Allowable permutations act on anything that structural permutations do.

Equations

• ConNF.Allowable.instMulActionAllowable = MulAction.compHom X ConNF.Allowable.toStructPerm

theorem ConNF.Allowable.toStructPerm_smul [ConNF.Params] {α : ConNF.TypeIndex} [ConNF.ModelData α] {X : Type u_1} [MulAction (ConNF.StructPerm α) X] (ρ : ConNF.Allowable α) (x : X) : ρ • x = ConNF.Allowable.toStructPerm ρ • x

@[simp]

theorem ConNF.Allowable.smul_support_max [ConNF.Params] {α : ConNF.TypeIndex} [ConNF.ModelData α] (ρ : ConNF.Allowable α) (S : ConNF.Support α) : (ρ • S).max = S.max

@[simp]

theorem ConNF.Allowable.smul_support_f [ConNF.Params] {α : ConNF.TypeIndex} [ConNF.ModelData α] (ρ : ConNF.Allowable α) (S : ConNF.Support α) (i : ConNF.κ) (hi : i < S.max) : (ρ • S).f i hi = ρ • S.f i hi

@[simp]

theorem ConNF.Allowable.smul_support_coe [ConNF.Params] {α : ConNF.TypeIndex} [ConNF.ModelData α] (ρ : ConNF.Allowable α) (S : ConNF.Support α) : ConNF.Enumeration.carrier (ρ • S) = ρ • ConNF.Enumeration.carrier S

theorem ConNF.Allowable.smul_mem_smul_support [ConNF.Params] {α : ConNF.TypeIndex} [ConNF.ModelData α] {S : ConNF.Support α} {c : ConNF.Address α} (h : c ∈ S) (ρ : ConNF.Allowable α) : ρ • c ∈ ρ • S

theorem ConNF.Allowable.smul_eq_of_smul_support_eq [ConNF.Params] {α : ConNF.TypeIndex} [ConNF.ModelData α] {S : ConNF.Support α} {ρ : ConNF.Allowable α} (hS : ρ • S = S) {c : ConNF.Address α} (hc : c ∈ S) : ρ • c = c

theorem ConNF.Allowable.smul_address [ConNF.Params] {α : ConNF.TypeIndex} [ConNF.ModelData α] {ρ : ConNF.Allowable α} {c : ConNF.Address α} : ρ • c = { path := c.path, value := ConNF.Allowable.toStructPerm ρ c.path • c.value }

Although we use often this in simp invocations, it is not given the @[simp] attribute so that it doesn't get used unnecessarily.

@[simp]

theorem ConNF.Allowable.smul_address_eq_iff [ConNF.Params] {α : ConNF.TypeIndex} [ConNF.ModelData α] {ρ : ConNF.Allowable α} {c : ConNF.Address α} : ρ • c = c ↔ ConNF.Allowable.toStructPerm ρ c.path • c.value = c.value

@[simp]

theorem ConNF.Allowable.smul_address_eq_smul_iff [ConNF.Params] {α : ConNF.TypeIndex} [ConNF.ModelData α] {ρ : ConNF.Allowable α} {ρ' : ConNF.Allowable α} {c : ConNF.Address α} : ρ • c = ρ' • c ↔ ConNF.Allowable.toStructPerm ρ c.path • c.value = ConNF.Allowable.toStructPerm ρ' c.path • c.value

theorem ConNF.ModelData.TSet.has_support [ConNF.Params] {α : ConNF.TypeIndex} [ConNF.ModelData α] (t : ConNF.TSet α) : ∃ (S : ConNF.Support α), MulAction.Supports (ConNF.Allowable α) (ConNF.Enumeration.carrier S) t

def ConNF.Atom.support [ConNF.Params] (a : ConNF.Atom) : ConNF.Support ⊥

The canonical support for an atom.

Equations

• a.support = ConNF.Enumeration.singleton { path := Quiver.Path.nil, value := Sum.inl a }

@[simp]

theorem ConNF.Atom.support_carrier [ConNF.Params] (a : ConNF.Atom) : ConNF.Enumeration.carrier a.support = {{ path := Quiver.Path.nil, value := Sum.inl a }}

theorem ConNF.Atom.support_supports [ConNF.Params] (a : ConNF.Atom) : MulAction.Supports ConNF.BasePerm (ConNF.Enumeration.carrier a.support) a

instance ConNF.Bot.modelData [ConNF.Params] : ConNF.ModelData ⊥

The model data at level ⊥ is constructed by taking the t-sets to be the atoms, and the allowable permutations to be the base permutations.

Equations

• ConNF.Bot.modelData = ConNF.ModelData.mk ConNF.Atom ConNF.BasePerm ConNF.Tree.toBotIso.toMonoidHom ⋯ ⋯ ConNF.StructSet.toBot.toEmbedding ⋯

theorem ConNF.TangleCoe.ext : ∀ {inst : ConNF.Params} {α : ConNF.Λ} {inst_1 : ConNF.ModelData ↑α} (x y : ConNF.TangleCoe α), x.set = y.set → x.support = y.support → x = y

theorem ConNF.TangleCoe.ext_iff : ∀ {inst : ConNF.Params} {α : ConNF.Λ} {inst_1 : ConNF.ModelData ↑α} (x y : ConNF.TangleCoe α), x = y ↔ x.set = y.set ∧ x.support = y.support

structure ConNF.TangleCoe [ConNF.Params] (α : ConNF.Λ) [ConNF.ModelData ↑α] : Type u

A t-set at level α together with a support for it. This is a specialisation of the notion of a tangle which will be defined for arbitrary type indices.

• set : ConNF.TSet ↑α
• support : ConNF.Support ↑α
• support_supports : MulAction.Supports (ConNF.Allowable ↑α) (ConNF.Enumeration.carrier self.support) self.set

theorem ConNF.TangleCoe.support_supports [ConNF.Params] {α : ConNF.Λ} [ConNF.ModelData ↑α] (self : ConNF.TangleCoe α) : MulAction.Supports (ConNF.Allowable ↑α) (ConNF.Enumeration.carrier self.support) self.set

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

If α is a proper type index, an α-tangle is t-set at level α, together with a support for it. If α = ⊥, then an α-tangle is an atom.

Equations

• ConNF.Tangle x✝ = match x✝, x with | some α, x => ConNF.TangleCoe α | none, x => ConNF.Atom

def ConNF.Tangle.support [ConNF.Params] {α : ConNF.TypeIndex} [ConNF.ModelData α] : ConNF.Tangle α → ConNF.Support α

Each tangle comes with a support. Since we could (a priori) have instances for [ModelData ⊥] other than that constructed above, it's possible that this isn't a support under the action of ⊥-allowable permutations. We will later define Tangle.support_supports_lt which gives the expected result under suitable hypotheses.

Equations

• x.support = match x✝¹, x✝, x with | some α, x, t => t.support | none, _i, a => ConNF.Atom.support a

instance ConNF.instMulActionAllowableSomeΛTangleCoe [ConNF.Params] (α : ConNF.Λ) [ConNF.ModelData ↑α] : MulAction (ConNF.Allowable ↑α) (ConNF.TangleCoe α)

Equations

• ConNF.instMulActionAllowableSomeΛTangleCoe α = MulAction.mk ⋯ ⋯

instance ConNF.instMulActionAllowableTangle [ConNF.Params] (α : ConNF.TypeIndex) [ConNF.ModelData α] : MulAction (ConNF.Allowable α) (ConNF.Tangle α)

Allowable permutations act on tangles.

Equations

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

class ConNF.PositionedTangles [ConNF.Params] (α : ConNF.TypeIndex) [ConNF.ModelData α] : Type u

Provides a position function for α-tangles, giving each tangle a unique position ν : μ. The existence of this injection proves that there are at most μ tangles at level α, and therefore at most μ t-sets. Since μ has a well-ordering, this induces a well-ordering on α-tangles: to compare two tangles, simply compare their images under this map.

• pos : ConNF.Tangle α ↪ ConNF.μ

instance ConNF.instPositionTangleμOfPositionedTangles [ConNF.Params] {α : ConNF.TypeIndex} [ConNF.ModelData α] [ConNF.PositionedTangles α] : ConNF.Position (ConNF.Tangle α) ConNF.μ

Equations

• ConNF.instPositionTangleμOfPositionedTangles = { pos := ConNF.PositionedTangles.pos }

class ConNF.TypedObjects [ConNF.Params] (α : ConNF.Λ) [ConNF.ModelData ↑α] : Type u

Allows us to encode near-litters as α-tangles. These maps are expected to cohere with the conditions given in BasePositions, but this requirement is expressed later.

• typedNearLitter : ConNF.NearLitter ↪ ConNF.TSet ↑α

  Encode a near-litter as an α-tangle. The resulting model element has a ⊥-extension which contains only this near-litter.

• smul_typedNearLitter : ∀ (ρ : ConNF.Allowable ↑α) (N : ConNF.NearLitter), ρ • ConNF.typedNearLitter N = ConNF.typedNearLitter (ConNF.Allowable.toStructPerm ρ (Quiver.Hom.toPath ⋯) • N)

theorem ConNF.TypedObjects.smul_typedNearLitter [ConNF.Params] {α : ConNF.Λ} [ConNF.ModelData ↑α] [self : ConNF.TypedObjects α] (ρ : ConNF.Allowable ↑α) (N : ConNF.NearLitter) : ρ • ConNF.typedNearLitter N = ConNF.typedNearLitter (ConNF.Allowable.toStructPerm ρ (Quiver.Hom.toPath ⋯) • N)

class ConNF.BasePositions [ConNF.Params] : Type u

Almost arbitrarily chosen position functions for atoms and near-litters. The only requirements they satisfy are included in this class. These requirements are later used to prove that the Constrains relation is well-founded.

• posAtom : ConNF.Atom ↪ ConNF.μ
• posNearLitter : ConNF.NearLitter ↪ ConNF.μ
• lt_pos_atom : ∀ (a : ConNF.Atom), ConNF.BasePositions.posNearLitter a.1.toNearLitter < ConNF.BasePositions.posAtom a
• lt_pos_litter : ∀ (N : ConNF.NearLitter), ¬N.IsLitter → ConNF.BasePositions.posNearLitter N.fst.toNearLitter < ConNF.BasePositions.posNearLitter N
• lt_pos_symmDiff : ∀ (a : ConNF.Atom) (N : ConNF.NearLitter), a ∈ symmDiff (ConNF.litterSet N.fst) ↑N → ConNF.BasePositions.posAtom a < ConNF.BasePositions.posNearLitter N

theorem ConNF.BasePositions.lt_pos_atom [ConNF.Params] [self : ConNF.BasePositions] (a : ConNF.Atom) : ConNF.BasePositions.posNearLitter a.1.toNearLitter < ConNF.BasePositions.posAtom a

theorem ConNF.BasePositions.lt_pos_litter [ConNF.Params] [self : ConNF.BasePositions] (N : ConNF.NearLitter) (hN : ¬N.IsLitter) : ConNF.BasePositions.posNearLitter N.fst.toNearLitter < ConNF.BasePositions.posNearLitter N

theorem ConNF.BasePositions.lt_pos_symmDiff [ConNF.Params] [self : ConNF.BasePositions] (a : ConNF.Atom) (N : ConNF.NearLitter) (h : a ∈ symmDiff (ConNF.litterSet N.fst) ↑N) : ConNF.BasePositions.posAtom a < ConNF.BasePositions.posNearLitter N

instance ConNF.instPositionAtomμOfBasePositions [ConNF.Params] [ConNF.BasePositions] : ConNF.Position ConNF.Atom ConNF.μ

A position function for atoms.

Equations

• ConNF.instPositionAtomμOfBasePositions = { pos := ConNF.BasePositions.posAtom }

instance ConNF.instPositionNearLitterμOfBasePositions [ConNF.Params] [ConNF.BasePositions] : ConNF.Position ConNF.NearLitter ConNF.μ

A position function for near-litters.

Equations

• ConNF.instPositionNearLitterμOfBasePositions = { pos := ConNF.BasePositions.posNearLitter }

theorem ConNF.lt_pos_atom [ConNF.Params] [ConNF.BasePositions] (a : ConNF.Atom) : ConNF.pos a.1.toNearLitter < ConNF.pos a

theorem ConNF.lt_pos_litter [ConNF.Params] [ConNF.BasePositions] (N : ConNF.NearLitter) (hN : ¬N.IsLitter) : ConNF.pos N.fst.toNearLitter < ConNF.pos N

theorem ConNF.lt_pos_symmDiff [ConNF.Params] [ConNF.BasePositions] (a : ConNF.Atom) (N : ConNF.NearLitter) (h : a ∈ symmDiff (ConNF.litterSet N.fst) ↑N) : ConNF.pos a < ConNF.pos N

class ConNF.PositionedObjects [ConNF.Params] (α : ConNF.Λ) [ConNF.ModelData ↑α] [ConNF.BasePositions] [ConNF.PositionedTangles ↑α] [ConNF.TypedObjects α] : Prop

The assertion that the position of typed near-litters is at least the position of the near-litter itself. This is used to prove that the alternative extension relation ↝ is well-founded.

• pos_typedNearLitter : ∀ (N : ConNF.NearLitter) (t : ConNF.Tangle ↑α), t.set = ConNF.typedNearLitter N → ConNF.pos N ≤ ConNF.pos t

theorem ConNF.PositionedObjects.pos_typedNearLitter [ConNF.Params] {α : ConNF.Λ} [ConNF.ModelData ↑α] [ConNF.BasePositions] [ConNF.PositionedTangles ↑α] [ConNF.TypedObjects α] [self : ConNF.PositionedObjects α] (N : ConNF.NearLitter) (t : ConNF.Tangle ↑α) : t.set = ConNF.typedNearLitter N → ConNF.pos N ≤ ConNF.pos t

theorem ConNF.Allowable.smul_typedNearLitter [ConNF.Params] {α : ConNF.Λ} [ConNF.ModelData ↑α] [ConNF.TypedObjects α] (ρ : ConNF.Allowable ↑α) (N : ConNF.NearLitter) : ρ • ConNF.typedNearLitter N = ConNF.typedNearLitter (ConNF.Allowable.toStructPerm ρ (Quiver.Hom.toPath ⋯) • N)

The action of allowable permutations on tangles commutes with the typedNearLitter function mapping near-litters to typed near-litters. This can be seen by representing tangles as codes.

instance ConNF.Bot.positionedTangles [ConNF.Params] [ConNF.BasePositions] : ConNF.PositionedTangles ⊥

The position function at level ⊥, taken from the BasePositions.

Equations

• ConNF.Bot.positionedTangles = { pos := ConNF.BasePositions.posAtom }

def BasePerm.ofBot [ConNF.Params] : ConNF.Allowable ⊥ ≃ ConNF.BasePerm

The identity equivalence between ⊥-allowable permutations and base permutations. This equivalence is a group isomorphism.

Equations

• BasePerm.ofBot = Equiv.refl (ConNF.Allowable ⊥)

@[simp]

theorem BasePerm.ofBot_smul [ConNF.Params] {X : Type u_1} [MulAction ConNF.BasePerm X] (π : ConNF.Allowable ⊥) (x : X) : BasePerm.ofBot π • x = π • x