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 [ConNF.Params] {X Y : Type u} {α : ConNF.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 [ConNF.Params] {X Y : Type u} {α : ConNF.TypeIndex} {f : α ↝ ⊥ → Rel X Y} (hf : ∀ (A : α ↝ ⊥), (f A).Coinjective) : (ConNF.Enumeration.relWithPath f).Coinjective

instance ConNF.Enumeration.instDerivativeProdPathBotTypeIndex [ConNF.Params] (X : Type u) (α β : ConNF.TypeIndex) : ConNF.Derivative (ConNF.Enumeration (α ↝ ⊥ × X)) (ConNF.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 [ConNF.Params] {X : Type u} {α β : ConNF.TypeIndex} (E : ConNF.Enumeration (α ↝ ⊥ × X)) (A : α ↝ β) (i : ConNF.κ) (x : β ↝ ⊥ × X) : (E ⇘ A).rel i x ↔ E.rel i (x.1 ⇗ A, x.2)

instance ConNF.Enumeration.instCoderivativeProdPathBotTypeIndex [ConNF.Params] (X : Type u) (α β : ConNF.TypeIndex) : ConNF.Coderivative (ConNF.Enumeration (β ↝ ⊥ × X)) (ConNF.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 [ConNF.Params] {X : Type u} {α β : ConNF.TypeIndex} (E : ConNF.Enumeration (β ↝ ⊥ × X)) (A : α ↝ β) (i : ConNF.κ) (x : α ↝ ⊥ × X) : (E ⇗ A).rel i x ↔ ∃ (B : β ↝ ⊥), x.1 = A ⇘ B ∧ E.rel i (B, x.2)

theorem ConNF.Enumeration.scoderiv_rel [ConNF.Params] {X : Type u} {α β : ConNF.TypeIndex} (E : ConNF.Enumeration (β ↝ ⊥ × X)) (h : β < α) (i : ConNF.κ) (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 [ConNF.Params] {X : Type u} {α β γ : ConNF.TypeIndex} (E : ConNF.Enumeration (β ↝ ⊥ × X)) (h : β < α) (h' : γ < α) (i : ConNF.κ) (A : γ ↝ ⊥) (x : X) : (E ↗ h).rel i (A ↗ h', x) → β = γ

instance ConNF.Enumeration.instBotDerivativeProdPathBotTypeIndex [ConNF.Params] (X : Type u) (α : ConNF.TypeIndex) : ConNF.BotDerivative (ConNF.Enumeration (α ↝ ⊥ × X)) (ConNF.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 [ConNF.Params] {X : Type u} {α : ConNF.TypeIndex} (E : ConNF.Enumeration (α ↝ ⊥ × X)) (A : α ↝ ⊥) (i : ConNF.κ) (x : X) : (E ⇘. A).rel i x ↔ E.rel i (A, x)

@[simp]

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

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

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

@[simp]

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

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

@[simp]

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

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

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

Equations

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

@[simp]

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

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

Equations

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

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

theorem ConNF.Enumeration.smul_eq_smul_of_forall_smul_eq [ConNF.Params] {X : Type u} {α : ConNF.TypeIndex} [MulAction ConNF.BasePerm X] {π₁ π₂ : ConNF.StrPerm α} {E : ConNF.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 [ConNF.Params] {X : Type u} {α : ConNF.TypeIndex} [MulAction ConNF.BasePerm X] {π : ConNF.StrPerm α} {E : ConNF.Enumeration (α ↝ ⊥ × X)} (h : π • E = E) (A : α ↝ ⊥) (x : X) (hx : (A, x) ∈ E) : π A • x = x

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