Documentation

TauCeti.Data.Sym.Pi

Unordered tuples with one point in each member of a family #

Given a family A : Fin n → Set α of subsets of a type, TauCeti.Sym.pi A is the set of unordered n-tuples obtained by choosing one point in each A i. When the members of the family are pairwise disjoint that choice is recorded faithfully: the unordered tuple remembers which of its points came from which member, so TauCeti.Sym.pi A is parametrized by the product ∀ i, ↥(A i) (TauCeti.Sym.piEquiv).

The case to keep in mind is the pair of tori T_α = α₁ × ⋯ × α_g and T_β = β₁ × ⋯ × β_g inside the symmetric power Sym^g(Σ) of a Heegaard surface, attached to the two systems of attaching curves of a Heegaard diagram (Ozsváth--Szabó, Holomorphic disks and topological invariants for closed three-manifolds, §2.1). The main result here describes their intersection: a point of T_α ∩ T_β is exactly a matching, a bijection σ of the index set together with a point of α_i ∩ β_{σ i} for each i. Consequently T_α ∩ T_β is finite as soon as the curves meet finitely often, and its cardinality is the permanent of the matrix of intersection numbers #(α_i ∩ β_j); these are the points that generate the Heegaard Floer chain complex. For a genus-one diagram the permanent degenerates to the number of intersection points of the two curves.

The parametrization by ordered tuples, its injectivity for a pairwise disjoint family, and the description of its range are TauCeti.Sym.ofFn_map_injective and TauCeti.Sym.mem_range_ofFn_map, which this file specializes to subtype coercions. Only the combinatorics of unordered tuples is used, so nothing here is topological; the corresponding statements about TauCeti.Sym.pi A as a subspace of the topological symmetric power are in TauCeti/Topology/Sym/Pi.lean.

Main declarations #

References #

One point in each member of a family #

source
def TauCeti.Sym.pi {α : Type u_1} {n : ℕ} (A : Fin n → Set α) :
Set (Sym α n)

The unordered n-tuples having one point in each member of a family A : Fin n → Set α of subsets, presented as the range of the parametrization by ordered tuples.

For the g attaching curves α₁, …, α_g of a Heegaard diagram on a surface Σ this is the torus T_α ⊆ Sym^g(Σ); the name follows Set.pi, of which it is the unordered analogue.

Equations
Instances For
    source
    theorem TauCeti.Sym.pi_eq_range {α : Type u_1} {n : ℕ} (A : Fin n → Set α) :
    pi A = Set.range fun (x : (i : Fin n) → ↑(A i)) => ofFn fun (i : Fin n) => ↑(x i)

    TauCeti.Sym.pi A is by definition the range of the parametrization by ordered tuples.

    source
    @[simp]
    theorem TauCeti.Sym.mem_pi_iff {α : Type u_1} {n : ℕ} {A : Fin n → Set α} {s : Sym α n} :
    s ∈ pi A ↔ ∃ (x : Fin n → α), (∀ (i : Fin n), x i ∈ A i) ∧ ofFn x = s

    An unordered tuple has one point in each member of the family exactly when it is presented by an ordered tuple whose i-th entry lies in A i.

    source
    theorem TauCeti.Sym.ofFn_mem_pi {α : Type u_1} {n : ℕ} {A : Fin n → Set α} {x : Fin n → α} (hx : ∀ (i : Fin n), x i ∈ A i) :
    ofFn x ∈ pi A

    An ordered tuple whose i-th entry lies in A i presents an unordered tuple with one point in each member of the family.

    source
    @[simp]
    theorem TauCeti.Sym.pi_comp_perm {α : Type u_1} {n : ℕ} {A : Fin n → Set α} (σ : Equiv.Perm (Fin n)) :
    pi (A ∘ ⇑σ) = pi A

    TauCeti.Sym.pi A only depends on the family up to reindexing: permuting the index set permutes the entries of an ordered presentation, which leaves the unordered tuple it presents unchanged.

    source
    @[simp]
    theorem TauCeti.Sym.pi_nonempty_iff {α : Type u_1} {n : ℕ} {A : Fin n → Set α} :
    (pi A).Nonempty ↔ ∀ (i : Fin n), (A i).Nonempty

    There is an unordered tuple with one point in each member of the family exactly when every member is nonempty.

    source
    theorem TauCeti.Sym.pi_eq_image_univ_pi {α : Type u_1} {n : ℕ} (A : Fin n → Set α) :
    pi A = ofFn '' Set.univ.pi A

    TauCeti.Sym.pi A is the image of the product Set.pi of the family under the quotient map from ordered tuples.

    source
    theorem TauCeti.Sym.disjoint_basepointDivisor_pi {α : Type u_1} {n : ℕ} {A : Fin n → Set α} {a : α} (ha : ∀ (i : Fin n), a ∉ A i) :
    Disjoint (basepointDivisor a) (pi A)

    The unordered tuples containing a point a that lies in no member of the family are disjoint from TauCeti.Sym.pi A. For a basepoint z of a Heegaard diagram, chosen off the attaching curves, this says that the divisor {z} × Sym^{g-1}(Σ) misses the torus T_α.

    Pairwise disjoint families #

    source
    theorem TauCeti.Sym.ofFn_subtypeVal_injective {α : Type u_1} {n : ℕ} {A : Fin n → Set α} (h : Pairwise (Function.onFun Disjoint A)) :
    Function.Injective fun (x : (i : Fin n) → ↑(A i)) => ofFn fun (i : Fin n) => ↑(x i)

    For a pairwise disjoint family, the ordered tuple with i-th entry in A i presenting a given unordered tuple is unique: no point can be attributed to two different members.

    source
    theorem TauCeti.Sym.ofFn_injOn_univ_pi {α : Type u_1} {n : ℕ} {A : Fin n → Set α} (h : Pairwise (Function.onFun Disjoint A)) :
    Set.InjOn ofFn (Set.univ.pi A)

    The Set.InjOn form of TauCeti.Sym.ofFn_subtypeVal_injective: for a pairwise disjoint family, two ordered tuples with i-th entry in A i presenting the same unordered tuple are equal.

    source
    theorem TauCeti.Sym.mem_pi_iff_card_filter {α : Type u_1} {n : ℕ} {A : Fin n → Set α} (h : Pairwise (Function.onFun Disjoint A)) {s : Sym α n} :
    s ∈ pi A ↔ ∀ (i : Fin n), (Multiset.filter (fun (x : α) => x ∈ A i) ↑s).card = 1

    For a pairwise disjoint family, membership in TauCeti.Sym.pi A is the condition that exactly one point of the unordered tuple lies in each member of the family.

    source
    noncomputable def TauCeti.Sym.piEquiv {α : Type u_1} {n : ℕ} {A : Fin n → Set α} (h : Pairwise (Function.onFun Disjoint A)) :
    ((i : Fin n) → ↑(A i)) ≃ ↑(pi A)

    The unordered tuples with one point in each member of a pairwise disjoint family are the product of its members. For the attaching curves of a Heegaard diagram this identifies T_α with α₁ × ⋯ × α_g.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.Sym.coe_piEquiv_apply {α : Type u_1} {n : ℕ} {A : Fin n → Set α} (h : Pairwise (Function.onFun Disjoint A)) (x : (i : Fin n) → ↑(A i)) :
      ↑((piEquiv h) x) = ofFn fun (i : Fin n) => ↑(x i)

      The parametrization underlying TauCeti.Sym.piEquiv is the one by ordered tuples.

      Matchings between two families #

      source
      theorem TauCeti.Sym.ofFn_mem_pi_inter_pi {α : Type u_1} {n : ℕ} {A B : Fin n → Set α} {σ : Equiv.Perm (Fin n)} {x : Fin n → α} (hA : ∀ (i : Fin n), x i ∈ A i) (hB : ∀ (i : Fin n), x i ∈ B (σ i)) :
      ofFn x ∈ pi A ∩ pi B

      An unordered tuple lies in both TauCeti.Sym.pi A and TauCeti.Sym.pi B as soon as it is presented by an ordered tuple with i-th entry in A i and in B (σ i), for a permutation σ of the index set.

      source
      theorem TauCeti.Sym.exists_perm_of_mem_pi_inter_pi {α : Type u_1} {n : ℕ} {A B : Fin n → Set α} {s : Sym α n} (hs : s ∈ pi A ∩ pi B) :
      ∃ (σ : Equiv.Perm (Fin n)) (x : Fin n → α), (∀ (i : Fin n), x i ∈ A i) ∧ (∀ (i : Fin n), x i ∈ B (σ i)) ∧ ofFn x = s

      Conversely, an unordered tuple lying in both TauCeti.Sym.pi A and TauCeti.Sym.pi B is presented by such an ordered tuple: the two presentations of it differ by a permutation.

      source
      def TauCeti.Sym.matchingTuple {α : Type u_1} {n : ℕ} {A B : Fin n → Set α} (p : (σ : Equiv.Perm (Fin n)) × ((i : Fin n) → ↑(A i ∩ B (σ i)))) :
      ↑(pi A ∩ pi B)

      The unordered tuple of a matching. A permutation σ of the index set together with a point of A i ∩ B (σ i) for each i determines an unordered tuple lying in both TauCeti.Sym.pi A and TauCeti.Sym.pi B.

      Equations
      Instances For
        source
        @[simp]
        theorem TauCeti.Sym.coe_matchingTuple_apply {α : Type u_1} {n : ℕ} {A B : Fin n → Set α} (p : (σ : Equiv.Perm (Fin n)) × ((i : Fin n) → ↑(A i ∩ B (σ i)))) :
        ↑(matchingTuple p) = ofFn fun (i : Fin n) => ↑(p.snd i)

        The unordered tuple of a matching is the tuple of its chosen points.

        source
        theorem TauCeti.Sym.matchingTuple_surjective {α : Type u_1} {n : ℕ} {A B : Fin n → Set α} :
        Function.Surjective matchingTuple

        Every unordered tuple lying in both TauCeti.Sym.pi A and TauCeti.Sym.pi B comes from a matching.

        source
        theorem TauCeti.Sym.matching_ext {α : Type u_1} {n : ℕ} {A B : Fin n → Set α} (hB : Pairwise (Function.onFun Disjoint B)) {p q : (σ : Equiv.Perm (Fin n)) × ((i : Fin n) → ↑(A i ∩ B (σ i)))} (h : ∀ (i : Fin n), ↑(p.snd i) = ↑(q.snd i)) :
        p = q

        Two matchings with the same chosen points are equal when the B-family is pairwise disjoint.

        source
        theorem TauCeti.Sym.matchingTuple_injective {α : Type u_1} {n : ℕ} {A B : Fin n → Set α} (hA : Pairwise (Function.onFun Disjoint A)) (hB : Pairwise (Function.onFun Disjoint B)) :
        Function.Injective matchingTuple

        For a pair of pairwise disjoint families, a matching is determined by the unordered tuple of its chosen points: the points determine the permutation, and the permutation determines them.

        source
        noncomputable def TauCeti.Sym.piInterEquiv {α : Type u_1} {n : ℕ} {A B : Fin n → Set α} (hA : Pairwise (Function.onFun Disjoint A)) (hB : Pairwise (Function.onFun Disjoint B)) :
        (σ : Equiv.Perm (Fin n)) × ((i : Fin n) → ↑(A i ∩ B (σ i))) ≃ ↑(pi A ∩ pi B)

        The points common to two tori are the matchings. For a pair of pairwise disjoint families, the unordered tuples with one point in each A i and one point in each B j correspond to the data of a permutation σ of the index set and a point of A i ∩ B (σ i) for each i.

        For the attaching curves of a Heegaard diagram this is the description of T_α ∩ T_β, whose points generate the Heegaard Floer chain complex.

        Equations
        Instances For
          source
          @[simp]
          theorem TauCeti.Sym.piInterEquiv_apply {α : Type u_1} {n : ℕ} {A B : Fin n → Set α} (hA : Pairwise (Function.onFun Disjoint A)) (hB : Pairwise (Function.onFun Disjoint B)) (p : (σ : Equiv.Perm (Fin n)) × ((i : Fin n) → ↑(A i ∩ B (σ i)))) :
          (piInterEquiv hA hB) p = matchingTuple p

          TauCeti.Sym.piInterEquiv sends a matching to its unordered tuple.

          Counting the common points #

          source
          theorem TauCeti.Sym.finite_pi_inter_pi {α : Type u_1} {n : ℕ} {A B : Fin n → Set α} (hfin : ∀ (i j : Fin n), (A i ∩ B j).Finite) :
          (pi A ∩ pi B).Finite

          Two tori meet in a finite set as soon as the members of the two families meet pairwise in finite sets: every common point is a matching, and there are finitely many of those.

          source
          theorem TauCeti.Sym.natCard_pi_inter_pi {α : Type u_1} {n : ℕ} {A B : Fin n → Set α} (hA : Pairwise (Function.onFun Disjoint A)) (hB : Pairwise (Function.onFun Disjoint B)) (hfin : ∀ (i j : Fin n), (A i ∩ B j).Finite) :
          Nat.card ↑(pi A ∩ pi B) = (Matrix.of fun (i j : Fin n) => Nat.card ↑(A i ∩ B j)).permanent

          The number of common points of two tori is the permanent of the matrix of intersection numbers. Summing over the matchings groups the common points by the permutation matching the members of the first family to those of the second.

          For the attaching curves of a Heegaard diagram this counts the generators of the Heegaard Floer chain complex.

          source
          theorem TauCeti.Sym.natCard_pi_inter_pi_fin_one {α : Type u_1} {A B : Fin 1 → Set α} :
          Nat.card ↑(pi A ∩ pi B) = Nat.card ↑(A 0 ∩ B 0)

          For a single pair of sets the permanent count degenerates to the number of common points: the generator count of a genus-one Heegaard diagram, carrying one attaching curve on each side. No finiteness is needed, the two sides being 0 together when the two curves meet infinitely often.