Axis-selection fibers

This module describes preimages of coordinate maps and proves the cardinality of fibers induced by selecting a duplicate-free tuple of axes.

@[reducible, inline]

abbrev TorchLean.Tensor.Internal.Fiber {ι : Type u} {κ : Type v} (f : ι → κ) (y : κ) : Type u

The preimage of y under f, represented as a finite subtype when the domain is finite.

noncomputable def TorchLean.Tensor.Internal.AxisTuple.selectFiberEquiv {ι : Type u} [BEq ι] [LawfulBEq ι] {length : ι → ℕ} {source target : List ι} (hSource : source.Nodup) (hTarget : target.Nodup) (hSourceTarget : ∀ axis ∈ source, axis ∈ target) (sourceCoordinate : AxisTuple length source) : Fiber (select hSourceTarget) sourceCoordinate ≃ AxisTuple length (List.filter (fun (axis : ι) => !source.contains axis) target)

The fiber of selecting source axes from a duplicate-free target tuple is equivalent to a tuple over the axes of target absent from source.

This is the structural statement behind both repeat multiplicities and reduction/contraction fibers. It includes the empty complement, which gives a singleton fiber, and complements containing a zero-length axis, which give an empty fiber.

@[simp]

theorem TorchLean.Tensor.Internal.AxisTuple.selectFiberEquiv_apply {ι : Type u} [BEq ι] [LawfulBEq ι] {length : ι → ℕ} {source target : List ι} (hSource : source.Nodup) (hTarget : target.Nodup) (hSourceTarget : ∀ axis ∈ source, axis ∈ target) (sourceCoordinate : AxisTuple length source) (coordinate : Fiber (select hSourceTarget) sourceCoordinate) : (selectFiberEquiv hSource hTarget hSourceTarget sourceCoordinate) coordinate = select ⋯ ↑coordinate

The free tuple returned by selectFiberEquiv consists of the target coordinates whose axes are absent from the selected source.

theorem TorchLean.Tensor.Internal.AxisTuple.select_fiber_card {ι : Type u} [BEq ι] [LawfulBEq ι] {length : ι → ℕ} {source target : List ι} (hSource : source.Nodup) (hTarget : target.Nodup) (hSourceTarget : ∀ axis ∈ source, axis ∈ target) (sourceCoordinate : AxisTuple length source) : Fintype.card (Fiber (select hSourceTarget) sourceCoordinate) = (List.map length (List.filter (fun (axis : ι) => !source.contains axis) target)).prod

The fiber of tuple selection has one free coordinate for every target axis absent from the source.

Consequently, its cardinality is the product of the introduced axis lengths. The empty product is one, while any introduced zero-length axis makes the fiber empty.