def Holor.map {α : Type u_1} {β : Type u_2} {ds : List ℕ} (f : α → β) (h : Holor α ds) : Holor β ds

Mapping is covariant in the value

Equations

• Holor.map f h = f ∘ h

theorem Holor.map_functorial {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ds : List ℕ} (f : α → β) (g : β → γ) (h : Holor α ds) : Holor.map g (Holor.map f h) = Holor.map (g ∘ f) h

def Holor.reindex {ds₂ : List ℕ} {ds₁ : List ℕ} {α : Type u_1} (ix : HolorIndex ds₂ → HolorIndex ds₁) (h : Holor α ds₁) : Holor α ds₂

Reindexing is contravariant in the index

Equations

• Holor.reindex ix h ix₂ = h (ix ix₂)

theorem Holor.reindex_functorial {ds₂ : List ℕ} {ds₁ : List ℕ} {ds₃ : List ℕ} {α : Type u_1} (ix : HolorIndex ds₂ → HolorIndex ds₁) (iy : HolorIndex ds₃ → HolorIndex ds₂) (h : Holor α ds₁) : Holor.reindex iy (Holor.reindex ix h) = Holor.reindex (ix ∘ iy) h

def Holor.pointwise_mul {α : Type u_1} {ds : List ℕ} [Mul α] (h₁ : Holor α ds) (h₂ : Holor α ds) : Holor α ds

Pointiwse multiplication of holors. Lifts multiplicative structure into holor.

Equations

• h₁.pointwise_mul h₂ ix = h₁ ix * h₂ ix

instance instMulHolor_sSA {α : Type u_1} {ds : List ℕ} [Mul α] : Mul (Holor α ds)

Equations

• instMulHolor_sSA = { mul := Holor.pointwise_mul }

theorem Holor.pointwise_mul_index {α : Type u_1} {ds : List ℕ} {i : HolorIndex ds} [Mul α] (h₁ : Holor α ds) (h₂ : Holor α ds) : (h₁ * h₂) i = h₁ i * h₂ i

instance instSemiringHolor_sSA {α : Type u_1} {ds : List ℕ} [Semiring α] : Semiring (Holor α ds)

Holor inherits algebraic structures -

Equations

• instSemiringHolor_sSA = id inferInstance

instance instCommSemiringHolor_sSA {α : Type u_1} {ds : List ℕ} [CommSemiring α] : CommSemiring (Holor α ds)

Equations

• instCommSemiringHolor_sSA = id inferInstance

instance instRingHolor_sSA {α : Type u_1} {ds : List ℕ} [Ring α] : Ring (Holor α ds)

Equations

• instRingHolor_sSA = id inferInstance

instance instCommRingHolor_sSA {α : Type u_1} {ds : List ℕ} [CommRing α] : CommRing (Holor α ds)

Equations

• instCommRingHolor_sSA = id inferInstance

instance instSMulHolor_sSA {M : Type u_1} {A : Type u_2} {ds : List ℕ} [SMul M A] : SMul M (Holor A ds)

Equations

• instSMulHolor_sSA = id inferInstance

def Holor.fill {α : Type u_1} {ds : List ℕ} (a : α) : Holor α ds

Fill a holor with a constant value 'a'.

Equations

• Holor.fill a x = a

instance instAlgebraHolor_sSA {R : Type u_1} {A : Type u_2} {ds : List ℕ} [CommSemiring R] [Semiring A] [Algebra R A] : Algebra R (Holor A ds)

Equations

• instAlgebraHolor_sSA = Pi.algebra (HolorIndex ds) fun (a : HolorIndex ds) => A