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
[ConNF.Params]
[ConNF.Level]
[ConNF.CoherentData]
{β : ConNF.TypeIndex}
[ConNF.LeLevel β]
(S : ConNF.Support β)
(ρ : ConNF.AllPerm β)
(A : β ↝ ⊥)
(a₁ a₂ : ConNF.Atom)
:
theorem
ConNF.Support.convNearLitters_smul_iff_left
[ConNF.Params]
[ConNF.Level]
[ConNF.CoherentData]
{β : ConNF.TypeIndex}
[ConNF.LeLevel β]
(S : ConNF.Support β)
(ρ : ConNF.AllPerm β)
(A : β ↝ ⊥)
(N₁ N₂ : ConNF.NearLitter)
:
theorem
ConNF.Support.smul_convAtoms_injective
[ConNF.Params]
[ConNF.Level]
[ConNF.CoherentData]
{β : ConNF.TypeIndex}
[ConNF.LeLevel β]
(S : ConNF.Support β)
(ρ : ConNF.AllPerm β)
(A : β ↝ ⊥)
:
(ConNF.convAtoms S (ρᵁ • S) A).Injective
theorem
ConNF.Support.atomMemRel_smul_le
[ConNF.Params]
[ConNF.Level]
[ConNF.CoherentData]
{β : ConNF.TypeIndex}
[ConNF.LeLevel β]
(S : ConNF.Support β)
(ρ : ConNF.AllPerm β)
(A : β ↝ ⊥)
:
ConNF.atomMemRel S A ≤ ConNF.atomMemRel (ρᵁ • S) A
theorem
ConNF.Support.inflexible_of_inflexible_smul
[ConNF.Params]
[ConNF.Level]
[ConNF.CoherentData]
{β : ConNF.TypeIndex}
[ConNF.LeLevel β]
(S : ConNF.Support β)
(ρ : ConNF.AllPerm β)
{A : β ↝ ⊥}
{N₁ N₂ : ConNF.NearLitter}
(h : ConNF.convNearLitters S (ρᵁ • S) A N₁ N₂)
(P : ConNF.InflexiblePath β)
(t : ConNF.Tangle P.δ)
(hA : A = P.A ↘ ⋯ ↘.)
(hN₁ : N₁ᴸ = ConNF.fuzz ⋯ t)
:
∃ (ρ' : ConNF.AllPerm P.δ), N₂ᴸ = ConNF.fuzz ⋯ (ρ' • t)
theorem
ConNF.Support.litter_eq_of_flexible_smul
[ConNF.Params]
[ConNF.Level]
[ConNF.CoherentData]
{β : ConNF.TypeIndex}
[ConNF.LeLevel β]
(S : ConNF.Support β)
(ρ : ConNF.AllPerm β)
{A : β ↝ ⊥}
{N₁ N₂ N₃ N₄ : ConNF.NearLitter}
(h₁₂ : ConNF.convNearLitters S (ρᵁ • S) A N₁ N₂)
(h₃₄ : ConNF.convNearLitters S (ρᵁ • S) A N₃ N₄)
(h₁₃ : N₁ᴸ = N₃ᴸ)
:
theorem
ConNF.Support.convNearLitters_fuzz
[ConNF.Params]
[ConNF.Level]
[ConNF.CoherentData]
{β : ConNF.TypeIndex}
[ConNF.LeLevel β]
(S : ConNF.Support β)
(ρ : ConNF.AllPerm β)
(A : β ↝ ⊥)
(N₁ N₂ : ConNF.NearLitter)
(P : ConNF.InflexiblePath β)
(t : ConNF.Tangle P.δ)
(ρ' : ConNF.AllPerm P.δ)
(hA : A = P.A ↘ ⋯ ↘.)
(hN₁ : N₁ᴸ = ConNF.fuzz ⋯ t)
(hN₂ : N₂ᴸ = ConNF.fuzz ⋯ (ρ' • t))
(hN : ConNF.convNearLitters S (ρᵁ • S) A N₁ N₂)
:
theorem
ConNF.Support.atoms_of_inflexible_smul
[ConNF.Params]
[ConNF.Level]
[ConNF.CoherentData]
{β : ConNF.TypeIndex}
[ConNF.LeLevel β]
(S : ConNF.Support β)
(ρ : ConNF.AllPerm β)
(A : β ↝ ⊥)
(N₁ N₂ : ConNF.NearLitter)
(P : ConNF.InflexiblePath β)
(t : ConNF.Tangle P.δ)
(ρ' : ConNF.AllPerm P.δ)
(hA : A = P.A ↘ ⋯ ↘.)
(hN₁ : N₁ᴸ = ConNF.fuzz ⋯ t)
(hN₂ : N₂ᴸ = ConNF.fuzz ⋯ (ρ' • t))
(hN : ConNF.convNearLitters S (ρᵁ • S) A N₁ N₂)
(B : P.δ ↝ ⊥)
(a : ConNF.Atom)
(ha : a ∈ (t.support ⇘. B)ᴬ)
(i : ConNF.κ)
(hiS : (S ⇘. (P.A ↘ ⋯ ⇘ B))ᴬ.rel i a)
:
theorem
ConNF.Support.nearLitters_of_inflexible_smul
[ConNF.Params]
[ConNF.Level]
[ConNF.CoherentData]
{β : ConNF.TypeIndex}
[ConNF.LeLevel β]
(S : ConNF.Support β)
(ρ : ConNF.AllPerm β)
(A : β ↝ ⊥)
(N₁ N₂ : ConNF.NearLitter)
(P : ConNF.InflexiblePath β)
(t : ConNF.Tangle P.δ)
(ρ' : ConNF.AllPerm P.δ)
(hA : A = P.A ↘ ⋯ ↘.)
(hN₁ : N₁ᴸ = ConNF.fuzz ⋯ t)
(hN₂ : N₂ᴸ = ConNF.fuzz ⋯ (ρ' • t))
(hN : ConNF.convNearLitters S (ρᵁ • S) A N₁ N₂)
(B : P.δ ↝ ⊥)
(N : ConNF.NearLitter)
(ha : N ∈ (t.support ⇘. B)ᴺ)
(i : ConNF.κ)
(hiS : (S ⇘. (P.A ↘ ⋯ ⇘ B))ᴺ.rel i N)
:
@[simp]
theorem
ConNF.Support.sameSpecLe_smul
[ConNF.Params]
[ConNF.Level]
[ConNF.CoherentData]
{β : ConNF.TypeIndex}
[ConNF.LeLevel β]
(S : ConNF.Support β)
(ρ : ConNF.AllPerm β)
:
ConNF.SameSpecLE S (ρᵁ • S)
@[simp]
theorem
ConNF.Support.smul_spec
[ConNF.Params]
[ConNF.Level]
[ConNF.CoherentData]
{β : ConNF.TypeIndex}
[ConNF.LeLevel β]
(S : ConNF.Support β)
(ρ : ConNF.AllPerm β)
: