Enumerations over paths

In this file, we provide extra features to Enumerations that take values of the form α ↝ ⊥ × X.

Main declarations

• ConNF.Enumeration.ext_path: An extensionality principle for such Enumerations.

def ConNF.Enumeration.relWithPath [Params] {X Y : Type u} {α : TypeIndex} (f : α ↝ ⊥ → Rel X Y) : Rel (α ↝ ⊥ × X) (α ↝ ⊥ × Y)

A helper function for making relations with domain and codomain of the form α ↝ ⊥ × X by defining it on each branch.

Equations

• ConNF.Enumeration.relWithPath f x y = (x.1 = y.1 ∧ f x.1 x.2 y.2)

theorem ConNF.Enumeration.relWithPath_coinjective [Params] {X Y : Type u} {α : TypeIndex} {f : α ↝ ⊥ → Rel X Y} (hf : ∀ (A : α ↝ ⊥), (f A).Coinjective) : (relWithPath f).Coinjective

instance ConNF.Enumeration.instDerivativeProdPathBotTypeIndex [Params] (X : Type u) (α β : TypeIndex) : Derivative (Enumeration (α ↝ ⊥ × X)) (Enumeration (β ↝ ⊥ × X)) α β

Equations

• ConNF.Enumeration.instDerivativeProdPathBotTypeIndex X α β = ConNF.Derivative.mk (fun (E : ConNF.Enumeration (α ↝ ⊥ × X)) (A : α ↝ β) => E.invImage (fun (x : β ↝ ⊥ × X) => (x.1 ⇗ A, x.2)) ⋯) ⋯

theorem ConNF.Enumeration.deriv_rel [Params] {X : Type u} {α β : TypeIndex} (E : Enumeration (α ↝ ⊥ × X)) (A : α ↝ β) (i : κ) (x : β ↝ ⊥ × X) : (E ⇘ A).rel i x ↔ E.rel i (x.1 ⇗ A, x.2)

instance ConNF.Enumeration.instCoderivativeProdPathBotTypeIndex [Params] (X : Type u) (α β : TypeIndex) : Coderivative (Enumeration (β ↝ ⊥ × X)) (Enumeration (α ↝ ⊥ × X)) α β

Equations

• ConNF.Enumeration.instCoderivativeProdPathBotTypeIndex X α β = ConNF.Coderivative.mk (fun (E : ConNF.Enumeration (β ↝ ⊥ × X)) (A : α ↝ β) => E.image fun (x : β ↝ ⊥ × X) => (x.1 ⇗ A, x.2)) ⋯

theorem ConNF.Enumeration.coderiv_rel [Params] {X : Type u} {α β : TypeIndex} (E : Enumeration (β ↝ ⊥ × X)) (A : α ↝ β) (i : κ) (x : α ↝ ⊥ × X) : (E ⇗ A).rel i x ↔ ∃ (B : β ↝ ⊥), x.1 = A ⇘ B ∧ E.rel i (B, x.2)

theorem ConNF.Enumeration.scoderiv_rel [Params] {X : Type u} {α β : TypeIndex} (E : Enumeration (β ↝ ⊥ × X)) (h : β < α) (i : κ) (x : α ↝ ⊥ × X) : (E ↗ h).rel i x ↔ ∃ (B : β ↝ ⊥), x.1 = B ↗ h ∧ E.rel i (B, x.2)

theorem ConNF.Enumeration.eq_of_scoderiv_mem [Params] {X : Type u} {α β γ : TypeIndex} (E : Enumeration (β ↝ ⊥ × X)) (h : β < α) (h' : γ < α) (i : κ) (A : γ ↝ ⊥) (x : X) : (E ↗ h).rel i (A ↗ h', x) → β = γ

instance ConNF.Enumeration.instBotDerivativeProdPathBotTypeIndex [Params] (X : Type u) (α : TypeIndex) : BotDerivative (Enumeration (α ↝ ⊥ × X)) (Enumeration X) α

Equations

• ConNF.Enumeration.instBotDerivativeProdPathBotTypeIndex X α = ConNF.BotDerivative.mk (fun (E : ConNF.Enumeration (α ↝ ⊥ × X)) (A : α ↝ ⊥) => E.invImage (fun (x : X) => (A, x)) ⋯) ⋯

theorem ConNF.Enumeration.derivBot_rel [Params] {X : Type u} {α : TypeIndex} (E : Enumeration (α ↝ ⊥ × X)) (A : α ↝ ⊥) (i : κ) (x : X) : (E ⇘. A).rel i x ↔ E.rel i (A, x)

@[simp]

theorem ConNF.Enumeration.mem_path_iff [Params] {X : Type u} {α : TypeIndex} (E : Enumeration (α ↝ ⊥ × X)) (A : α ↝ ⊥) (x : X) : (A, x) ∈ E ↔ x ∈ E ⇘. A

theorem ConNF.Enumeration.ext_path [Params] {X : Type u} {α : TypeIndex} {E F : Enumeration (α ↝ ⊥ × X)} (h : ∀ (A : α ↝ ⊥), E ⇘. A = F ⇘. A) : E = F

theorem ConNF.Enumeration.deriv_derivBot [Params] {X : Type u} {α β : TypeIndex} (E : Enumeration (α ↝ ⊥ × X)) (A : α ↝ β) (B : β ↝ ⊥) : E ⇘ A ⇘. B = E ⇘. (A ⇘ B)

@[simp]

theorem ConNF.Enumeration.coderiv_deriv_eq [Params] {X : Type u} {α β : TypeIndex} (E : Enumeration (β ↝ ⊥ × X)) (A : α ↝ β) : E ⇗ A ⇘ A = E

theorem ConNF.Enumeration.eq_of_mem_scoderiv_botDeriv [Params] {X : Type u} {α β : TypeIndex} {S : Enumeration (β ↝ ⊥ × X)} {A : α ↝ ⊥} {h : β < α} {x : X} (hx : x ∈ S ↗ h ⇘. A) : ∃ (B : β ↝ ⊥), A = B ↗ h

@[simp]

theorem ConNF.Enumeration.scoderiv_botDeriv_eq [Params] {X : Type u} {α β : TypeIndex} (S : Enumeration (β ↝ ⊥ × X)) (A : β ↝ ⊥) (h : β < α) : S ↗ h ⇘. (A ↗ h) = S ⇘. A

theorem ConNF.Enumeration.mulAction_aux [Params] {X : Type u_1} {α : TypeIndex} [MulAction BasePerm X] (π : StrPerm α) : Function.Injective fun (x : α ↝ ⊥ × X) => (x.1, (π x.1)⁻¹ • x.2)

instance ConNF.Enumeration.instSMulStrPermProdPathBotTypeIndexOfMulActionBasePerm [Params] {X : Type u} {α : TypeIndex} [MulAction BasePerm X] : SMul (StrPerm α) (Enumeration (α ↝ ⊥ × X))

Equations

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

@[simp]

theorem ConNF.Enumeration.smulPath_rel [Params] {X : Type u} {α : TypeIndex} [MulAction BasePerm X] (π : StrPerm α) (E : Enumeration (α ↝ ⊥ × X)) (i : κ) (x : α ↝ ⊥ × X) : (π • E).rel i x ↔ E.rel i (x.1, (π x.1)⁻¹ • x.2)

instance ConNF.Enumeration.instMulActionStrPermProdPathBotTypeIndexOfBasePerm [Params] {X : Type u} {α : TypeIndex} [MulAction BasePerm X] : MulAction (StrPerm α) (Enumeration (α ↝ ⊥ × X))

Equations

• ConNF.Enumeration.instMulActionStrPermProdPathBotTypeIndexOfBasePerm = MulAction.mk ⋯ ⋯

theorem ConNF.Enumeration.smul_eq_of_forall_smul_eq [Params] {X : Type u} {α : TypeIndex} [MulAction BasePerm X] {π : StrPerm α} {E : Enumeration (α ↝ ⊥ × X)} (h : ∀ (A : α ↝ ⊥) (x : X), (A, x) ∈ E → π A • x = x) : π • E = E

theorem ConNF.Enumeration.smul_eq_smul_of_forall_smul_eq [Params] {X : Type u} {α : TypeIndex} [MulAction BasePerm X] {π₁ π₂ : StrPerm α} {E : Enumeration (α ↝ ⊥ × X)} (h : ∀ (A : α ↝ ⊥) (x : X), (A, x) ∈ E → π₁ A • x = π₂ A • x) : π₁ • E = π₂ • E

theorem ConNF.Enumeration.smul_eq_of_mem_of_smul_eq [Params] {X : Type u} {α : TypeIndex} [MulAction BasePerm X] {π : StrPerm α} {E : Enumeration (α ↝ ⊥ × X)} (h : π • E = E) (A : α ↝ ⊥) (x : X) (hx : (A, x) ∈ E) : π A • x = x

theorem ConNF.Enumeration.smul_eq_iff [Params] {X : Type u} {α : TypeIndex} [MulAction BasePerm X] (π : StrPerm α) (E : Enumeration (α ↝ ⊥ × X)) : π • E = E ↔ ∀ (A : α ↝ ⊥) (x : X), (A, x) ∈ E → π A • x = x