Documentation

TauCeti.Data.Sym.Basic

Basic lemmas for symmetric powers #

This file records small API extensions for Mathlib's symmetric powers, and the map TauCeti.Sym.ofFn reading an ordered n-tuple f : Fin n → α as an unordered one.

ofFn presents Sym α n as a quotient of Fin n → α: it is surjective, and its fibres are the orbits of the permutation action, by TauCeti.Sym.ofFn_eq_ofFn_iff. Nothing here is topological; TauCeti/Topology/Sym/Basic.lean uses this to give Sym α n the quotient topology coinduced along ofFn.

Main declarations #

source
@[simp]
theorem Sym.map_append {X : Type u_1} {Y : Type u_2} {d e : ℕ} (f : X → Y) (s : Sym X d) (t : Sym X e) :
map f (s.append t) = (map f s).append (map f t)

Mapping a function over an appended symmetric-power point is the append of the mapped symmetric-power points.

Ordered tuples as unordered ones #

source
def TauCeti.Sym.ofFn {α : Type u_1} {n : ℕ} (f : Fin n → α) :
Sym α n

The ordered n-tuple f : Fin n → α read as an unordered n-tuple.

This is Mathlib's quotient map Sym.ofVector precomposed with List.Vector.ofFn; the Fin n → α form is the one that carries a product topology, so it is the map that Sym α n carries the quotient topology along in TauCeti/Topology/Sym/Basic.lean.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.Sym.coe_ofFn {α : Type u_1} {n : ℕ} (f : Fin n → α) :
    ↑(ofFn f) = ↑(List.ofFn f)

    The multiset underlying ofFn f is the list of values of f.

    source
    theorem TauCeti.Sym.count_coe_ofFn {α : Type u_1} {n : ℕ} [DecidableEq α] (f : Fin n → α) (a : α) :
    Multiset.count a ↑(ofFn f) = {i : Fin n | f i = a}.card

    The multiplicity of a value in ofFn f is the number of entries of f equal to it.

    source
    @[simp]
    theorem TauCeti.Sym.mem_ofFn {α : Type u_1} {n : ℕ} {a : α} {f : Fin n → α} :
    a ∈ ofFn f ↔ ∃ (i : Fin n), f i = a

    The points of ofFn f are exactly the values of f.

    source
    theorem TauCeti.Sym.ofFn_surjective {α : Type u_1} {n : ℕ} :
    Function.Surjective ofFn

    Every unordered n-tuple is the image of an ordered one: ofFn is the quotient map presenting Sym α n as a quotient of Fin n → α.

    source
    @[simp]
    theorem TauCeti.Sym.ofFn_cons {α : Type u_1} {n : ℕ} (a : α) (f : Fin n → α) :
    ofFn (Fin.cons a f) = a ::ₛ ofFn f

    Prepending a point to an ordered tuple adjoins it to the unordered one.

    source
    @[simp]
    theorem TauCeti.Sym.map_ofFn {α : Type u_1} {β : Type u_2} {n : ℕ} (f : α → β) (g : Fin n → α) :
    Sym.map f (ofFn g) = ofFn (f ∘ g)

    Applying a function to every entry of an ordered tuple applies it to every point of the unordered one.

    source
    theorem TauCeti.Sym.map_comp_ofFn {α : Type u_1} {β : Type u_2} {n : ℕ} (f : α → β) :
    Sym.map f ∘ ofFn = ofFn ∘ Pi.map fun (x : Fin n) => f

    The compatibility of Sym.map with ofFn, as an equality of maps out of ordered tuples.

    source
    theorem TauCeti.Sym.mem_range_map {α : Type u_1} {β : Type u_2} {n : ℕ} (f : α → β) {w : Sym β n} :
    w ∈ Set.range (Sym.map f) ↔ ∀ b ∈ w, b ∈ Set.range f

    The range of the map on symmetric powers consists of the unordered tuples whose every point lies in the range of the original map.

    source
    @[simp]
    theorem TauCeti.Sym.ofFn_fin_append {α : Type u_1} {m n : ℕ} (f : Fin m → α) (g : Fin n → α) :
    ofFn (Fin.append f g) = (ofFn f).append (ofFn g)

    Concatenating two ordered tuples adjoins the two unordered ones.

    The fibres of the quotient map #

    source
    theorem TauCeti.Sym.ofFn_comp_perm {α : Type u_1} {n : ℕ} (σ : Equiv.Perm (Fin n)) (f : Fin n → α) :
    ofFn (f ∘ ⇑σ) = ofFn f

    Reindexing an ordered tuple by a permutation leaves the underlying unordered tuple unchanged.

    source
    theorem TauCeti.Sym.ofFn_eq_ofFn_iff {α : Type u_1} {n : ℕ} {f g : Fin n → α} :
    ofFn f = ofFn g ↔ ∃ (σ : Equiv.Perm (Fin n)), f ∘ ⇑σ = g

    Two ordered tuples have the same underlying unordered tuple exactly when one is a reindexing of the other: the fibres of ofFn are the orbits of the permutation action.

    Adjoining a fixed point #

    source
    def TauCeti.Sym.basepointDivisor {α : Type u_1} {n : ℕ} (a : α) :
    Set (Sym α n)

    The divisor of unordered tuples containing the fixed point a.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.Sym.mem_basepointDivisor {α : Type u_1} {n : ℕ} {a : α} {s : Sym α n} :
      s ∈ basepointDivisor a ↔ a ∈ s
      source
      @[simp]
      theorem TauCeti.Sym.basepointDivisor_zero {α : Type u_1} (a : α) :
      basepointDivisor a = ∅

      No unordered tuple of length zero contains a point.

      source
      @[simp]
      theorem TauCeti.Sym.range_cons {α : Type u_1} {n : ℕ} (a : α) :
      Set.range (Sym.cons a) = basepointDivisor a

      The unordered (n + 1)-tuples obtained by adjoining the point a are exactly those that contain a.

      Unordered tuples over a two-element type #

      source
      noncomputable def TauCeti.symFinTwoEquiv (d : ℕ) :
      Sym (Fin 2) d ≃ Fin (d + 1)

      A multiset of size d over Fin 2 is determined by how many of its entries are 0, and that count can be anything from 0 to d: the two counts sum to d, so the pair of them runs over the antidiagonal of d. This is the rank-two instance of the count #(Sym α d) = (#α + d - 1).choose d.

      Equations
      Instances For
        source
        @[simp]
        theorem TauCeti.coe_symFinTwoEquiv_apply (d : ℕ) (s : Sym (Fin 2) d) :
        ↑((symFinTwoEquiv d) s) = Multiset.count 0 ↑s

        TauCeti.symFinTwoEquiv is the number of entries equal to 0.

        source
        @[simp]
        theorem TauCeti.coe_symFinTwoEquiv_symm_apply (d : ℕ) (i : Fin (d + 1)) :
        ↑((symFinTwoEquiv d).symm i) = Multiset.replicate (↑i) 0 + Multiset.replicate (d - ↑i) 1

        The inverse of TauCeti.symFinTwoEquiv spelled out: i many 0s and d - i many 1s.