Finite-fiber values

Finite fibers can be summed or collected as multisets. The transport theorems here compare fibers under equivalences and composition independently of tensor syntax.

@[instance_reducible]

instance TorchLean.Tensor.Internal.Fiber.equivUnique {ι : Type u} {κ : Type v} (e : ι ≃ κ) (y : κ) : Unique (Fiber (⇑e) y)

Every fiber of an equivalence has a unique element.

theorem TorchLean.Tensor.Internal.Fiber.card_equiv {ι : Type u} {κ : Type v} [Fintype ι] [DecidableEq κ] (e : ι ≃ κ) (y : κ) : Fintype.card (Fiber (⇑e) y) = 1

The fiber of an equivalence has cardinality one.

def TorchLean.Tensor.Internal.Fiber.sum {ι : Type u} {κ : Type v} {α : Type u_1} [Fintype ι] [DecidableEq κ] [AddCommMonoid α] (f : ι → κ) (y : κ) (x : ι → α) : α

Add all values indexed by one finite fiber.

def TorchLean.Tensor.Internal.Fiber.values {ι : Type u} {κ : Type v} {α : Type u_1} [Fintype ι] [DecidableEq κ] (f : ι → κ) (outputCoordinate : κ) (input : ι → α) : Multiset α

The multiset of input values in one finite fiber.

Using a multiset records multiplicity while deliberately forgetting enumeration order. A reduction may therefore change scalar type and need not be presented as a binary operation with an identity.

@[simp]

theorem TorchLean.Tensor.Internal.Fiber.values_card {ι : Type u} {κ : Type v} {α : Type u_1} [Fintype ι] [DecidableEq κ] (f : ι → κ) (outputCoordinate : κ) (input : ι → α) : (values f outputCoordinate input).card = Fintype.card (Fiber f outputCoordinate)

A fiber's value multiset has one entry for every coordinate in the fiber.

@[simp]

theorem TorchLean.Tensor.Internal.Fiber.values_sum {ι : Type u} {κ : Type v} {R : Type u_1} [Fintype ι] [DecidableEq κ] [AddCommMonoid R] (f : ι → κ) (outputCoordinate : κ) (input : ι → R) : (values f outputCoordinate input).sum = ∑ inputCoordinate : Fiber f outputCoordinate, input ↑inputCoordinate

Summing a fiber's value multiset is the corresponding finite coordinate sum.

@[simp]

theorem TorchLean.Tensor.Internal.Fiber.values_prod {ι : Type u} {κ : Type v} {R : Type u_1} [Fintype ι] [DecidableEq κ] [CommMonoid R] (f : ι → κ) (outputCoordinate : κ) (input : ι → R) : (values f outputCoordinate input).prod = ∏ inputCoordinate : Fiber f outputCoordinate, input ↑inputCoordinate

Multiplying a fiber's value multiset is the corresponding finite coordinate product.

theorem TorchLean.Tensor.Internal.Fiber.values_comp_equiv {ι : Type u} {κ : Type v} {τ : Type u_1} {α : Type u_2} [Fintype ι] [Fintype κ] [DecidableEq τ] (e : ι ≃ κ) (f : ι → τ) (outputCoordinate : τ) (input : κ → α) : values f outputCoordinate (input ∘ ⇑e) = values (f ∘ ⇑e.symm) outputCoordinate input

Changing the domain of a fiber by an equivalence preserves its multiset of values.

theorem TorchLean.Tensor.Internal.Fiber.values_target_equiv {ι : Type u} {κ : Type v} {τ : Type u_1} {α : Type u_2} [Fintype ι] [DecidableEq κ] [DecidableEq τ] (e : κ ≃ τ) (f : ι → κ) (outputCoordinate : τ) (input : ι → α) : values f (e.symm outputCoordinate) input = values (⇑e ∘ f) outputCoordinate input

Transporting the target of a coordinate map by an equivalence preserves the corresponding fiber values.

theorem TorchLean.Tensor.Internal.Fiber.card_comp_equiv {ι : Type u} {κ : Type v} {τ : Type u_1} [Fintype ι] [Fintype κ] [DecidableEq τ] (e : ι ≃ κ) (f : ι → τ) (outputCoordinate : τ) : Fintype.card (Fiber f outputCoordinate) = Fintype.card (Fiber (f ∘ ⇑e.symm) outputCoordinate)

Renaming a fiber's input coordinates preserves its cardinality.

theorem TorchLean.Tensor.Internal.Fiber.card_target_equiv {ι : Type u} {κ : Type v} {τ : Type u_1} [Fintype ι] [DecidableEq κ] [DecidableEq τ] (e : κ ≃ τ) (f : ι → κ) (outputCoordinate : τ) : Fintype.card (Fiber f (e.symm outputCoordinate)) = Fintype.card (Fiber (⇑e ∘ f) outputCoordinate)

Transporting a fiber's target by an equivalence preserves its cardinality.