Action on specifications

In this file, we prove that the specification of a support is invariant under the action of allowable permutations.

Main declarations

• ConNF.Support.smul_spec: The specification of a support is invariant under the action of allowable permutations.

theorem ConNF.Support.convAtoms_smul_iff_left [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] (S : Support β) (ρ : AllPerm β) (A : β ↝ ⊥) (a₁ a₂ : Atom) : convAtoms S (ρᵁ • S) A a₁ a₂ ↔ a₁ ∈ (S ⇘. A)ᴬ ∧ a₂ = ρᵁ A • a₁

theorem ConNF.Support.convNearLitters_smul_iff_left [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] (S : Support β) (ρ : AllPerm β) (A : β ↝ ⊥) (N₁ N₂ : NearLitter) : convNearLitters S (ρᵁ • S) A N₁ N₂ ↔ N₁ ∈ (S ⇘. A)ᴺ ∧ N₂ = ρᵁ A • N₁

theorem ConNF.Support.smul_convAtoms_injective [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] (S : Support β) (ρ : AllPerm β) (A : β ↝ ⊥) : (convAtoms S (ρᵁ • S) A).Injective

theorem ConNF.Support.atomMemRel_smul_le [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] (S : Support β) (ρ : AllPerm β) (A : β ↝ ⊥) : atomMemRel S A ≤ atomMemRel (ρᵁ • S) A

theorem ConNF.Support.inflexible_of_inflexible_smul [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] (S : Support β) (ρ : AllPerm β) {A : β ↝ ⊥} {N₁ N₂ : NearLitter} (h : convNearLitters S (ρᵁ • S) A N₁ N₂) (P : InflexiblePath β) (t : Tangle P.δ) (hA : A = P.A ↘ ⋯ ↘.) (hN₁ : N₁ᴸ = fuzz ⋯ t) : ∃ (ρ' : AllPerm P.δ), N₂ᴸ = fuzz ⋯ (ρ' • t)

theorem ConNF.Support.litter_eq_of_flexible_smul [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] (S : Support β) (ρ : AllPerm β) {A : β ↝ ⊥} {N₁ N₂ N₃ N₄ : NearLitter} (h₁₂ : convNearLitters S (ρᵁ • S) A N₁ N₂) (h₃₄ : convNearLitters S (ρᵁ • S) A N₃ N₄) (h₁₃ : N₁ᴸ = N₃ᴸ) : N₂ᴸ = N₄ᴸ

theorem ConNF.Support.convNearLitters_fuzz [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] (S : Support β) (ρ : AllPerm β) (A : β ↝ ⊥) (N₁ N₂ : NearLitter) (P : InflexiblePath β) (t : Tangle P.δ) (ρ' : AllPerm P.δ) (hA : A = P.A ↘ ⋯ ↘.) (hN₁ : N₁ᴸ = fuzz ⋯ t) (hN₂ : N₂ᴸ = fuzz ⋯ (ρ' • t)) (hN : convNearLitters S (ρᵁ • S) A N₁ N₂) : ρ' • t = ρ ⇘ P.A ↘ ⋯ • t

theorem ConNF.Support.atoms_of_inflexible_smul [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] (S : Support β) (ρ : AllPerm β) (A : β ↝ ⊥) (N₁ N₂ : NearLitter) (P : InflexiblePath β) (t : Tangle P.δ) (ρ' : AllPerm P.δ) (hA : A = P.A ↘ ⋯ ↘.) (hN₁ : N₁ᴸ = fuzz ⋯ t) (hN₂ : N₂ᴸ = fuzz ⋯ (ρ' • t)) (hN : convNearLitters S (ρᵁ • S) A N₁ N₂) (B : P.δ ↝ ⊥) (a : Atom) (ha : a ∈ (t.support ⇘. B)ᴬ) (i : κ) (hiS : (S ⇘. (P.A ↘ ⋯ ⇘ B))ᴬ.rel i a) : ((ρᵁ • S) ⇘. (P.A ↘ ⋯ ⇘ B))ᴬ.rel i (ρ'ᵁ B • a)

theorem ConNF.Support.nearLitters_of_inflexible_smul [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] (S : Support β) (ρ : AllPerm β) (A : β ↝ ⊥) (N₁ N₂ : NearLitter) (P : InflexiblePath β) (t : Tangle P.δ) (ρ' : AllPerm P.δ) (hA : A = P.A ↘ ⋯ ↘.) (hN₁ : N₁ᴸ = fuzz ⋯ t) (hN₂ : N₂ᴸ = fuzz ⋯ (ρ' • t)) (hN : convNearLitters S (ρᵁ • S) A N₁ N₂) (B : P.δ ↝ ⊥) (N : NearLitter) (ha : N ∈ (t.support ⇘. B)ᴺ) (i : κ) (hiS : (S ⇘. (P.A ↘ ⋯ ⇘ B))ᴺ.rel i N) : ((ρᵁ • S) ⇘. (P.A ↘ ⋯ ⇘ B))ᴺ.rel i (ρ'ᵁ B • N)

@[simp]

theorem ConNF.Support.sameSpecLe_smul [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] (S : Support β) (ρ : AllPerm β) : SameSpecLE S (ρᵁ • S)

@[simp]

theorem ConNF.Support.smul_spec [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] (S : Support β) (ρ : AllPerm β) : (ρᵁ • S).spec = S.spec