Library Combi.Combi.fibered_set: Bijection beetween fibered sets

Bijection beetween fibered sets

Given a type with equality I a fiberedset is a set fbset in an ihnabited fintype T equiped with a function fbfun : fbset -> I. The preimage of some i under fbfun is called the fiber of i. The goal of this file is to show that if two fibered set S1 S2 have their fiber of i of the same cardinality for all i, then there there exists a bijection fbbij from S1 to S2 which sends the fiber of i to the fiber of i. That is fbbij commute with the fbfun : forall x, fbfun2 (fbbij x) = fbfun1 x.
  • fibered_set == record for fibered sets on a carrier finType
  • fiber S i == the i-fiber of S
  • fbbij U V == a bijection from U to V provided the two fibered sets U and V have their fiber of i of the same cardinality:
    Hypothesis HcardEq : forall i, #|fiber U i| = #|fiber V i|.
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp Require Import ssrfun ssrbool eqtype ssrnat seq fintype finset.

Set Implicit Arguments.

Section BijFiberedSet.

Variable I : eqType.

Record fibered_set := FiberedSet {
                          carrier : finType;
                          elt : carrier;
                          fbset :> {set carrier};
                          fbfun : carrier -> I }.

Definition fiber (S : fibered_set) v := [set x | x in S & fbfun x == v].

Lemma mem_fiber (S : fibered_set) x : x \in S -> x \in fiber S (fbfun x).

Definition fbbij (U V : fibered_set) (x : carrier U) : carrier V :=
  nth (elt V) (enum (fiber V (fbfun x))) (index x (enum (fiber U (fbfun x)))).

Section Defs.

Variable U V : fibered_set.
Hypothesis HcardEq : forall i, #|fiber U i| = #|fiber V i|.

Lemma fbbij_in_fiber x : x \in U -> fbbij V x \in fiber V (fbfun x).

Lemma fbset_fbbij x : x \in U -> fbbij V x \in V.

Lemma equi_fbbij x : x \in U -> fbfun (fbbij V x) = fbfun x.

Lemma fbbijK : {in U, cancel (fbbij V) (fbbij U)}.

End Defs.

Lemma fbbijP (U V : fibered_set) :
  (forall i, #|fiber U i| = #|fiber V i|) ->
  [/\ {in U &, injective (fbbij V)},
   [set fbbij V x | x in U] = V &
   {in U, forall x, fbfun (fbbij V x) = fbfun x} ].

End BijFiberedSet.