Hugging Face's logo

Snapkitty
/
sovereign-array

custom
code
sovereign-compute
Model card Files
xet
 Community
sovereign-array
File size: 1,499 Bytes
d0f179a
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
/-!
# Broadcasting as Pullback

Broadcasting = pullback along projection `Ο€ : J β†’ I`.
`broadcast(f, Ο€) = f ∘ Ο€` is the categorical semantics of broadcasting.
-/

import ArrayLang.Array

namespace SovereignArray

/-- General pullback along a projection. `pullback Ο€ f = f ∘ Ο€`. -/
def pullback {I J : Type*} (Ο€ : J β†’ I) (f : I β†’ Ξ±) : J β†’ Ξ± := f ∘ Ο€

/-- Broadcasting: align `v` (indexed by `I`) to `J` via `Ο€`, then add `w` (indexed by `J`).
This is the `Ξ `-map `fun j => v (Ο€ j) + w j`. -/
def broadcast {Ξ± : Type*} [Add Ξ±] {I J : Type*} (Ο€ : J β†’ I)
    (v : I β†’ Ξ±) (w : J β†’ Ξ±) : J β†’ Ξ± :=
  fun j => v (Ο€ j) + w j

/-- The definition is literally the pullback-plus-add form. -/
theorem broadcast_is_pullback {Ξ± : Type*} [Add Ξ±] {I J : Type*} (Ο€ : J β†’ I) :
    (fun (v : I β†’ Ξ±) (w : J β†’ Ξ±) => broadcast Ο€ v w) =
    (fun v w j => v (Ο€ j) + w j) := rfl

/-- `broadcast` is `pullback Ο€ v` added pointwise to `w`. -/
theorem broadcast_eq_pullback {Ξ± : Type*} [Add Ξ±] {I J : Type*} (Ο€ : J β†’ I)
    (v : I β†’ Ξ±) (w : J β†’ Ξ±) :
    broadcast Ο€ v w = fun j => pullback Ο€ v j + w j := rfl

/-- Two successive broadcasts along `Ο€β‚‚ ∘ π₁` fuse into one pullback. -/
theorem broadcast_comp {Ξ± : Type*} [Add Ξ±] {I J K : Type*}
    (π₁ : J β†’ I) (Ο€β‚‚ : K β†’ J) (v : I β†’ Ξ±) (w : K β†’ Ξ±) :
    broadcast Ο€β‚‚ (pullback π₁ v) w = broadcast (π₁ ∘ Ο€β‚‚) v w := rfl

end SovereignArray