BUNDLE

Bundle package contains basic information about fibers (needed for weak-equivalence) and fiber bundles, constructions from algebraic topology.

Fiber

Definition (Fiber). The fiber of the map $p: E \rightarrow B$ in a point $y: B$ is all points $x: E$ such that $p(x)=y$.

fiber (E B: U) (p: E -> B) (y: B): U
    = (x: E) * Path B y (p x)

Fiber Bundle

Definition (Fiber Bundle). The fiber bundle $ F \rightarrow E \mapright{p} B$ on a total space $E$ with fiber layer $F$ and base $B$ is a structure $(F,E,p,B)$ where $p: E \rightarrow B$ is a surjective map with following property: for any point $y: B$ exists a neighborhood $U_b$ for which a homeomorphism $f: p^{-1}(U_b) \rightarrow U_b \times F$ making the following diagram commute.

$$ \begin{array}{ccc} p^{-1}(U_b) & \mapright{f} & U_b \times F \\ \mapdown{\mathbf{p}} & \mapdiagr{pr_1} & \\ U_b & & \\ \end{array} $$

Trivial Fiber Bundle

Definition (Trivial Fiber Bundle). When total space $E$ is cartesian product $\Sigma(B,F)$ and $p = pr_1$ then such bundle is called trivial $(F,\Sigma(B,F),pr_1,B)$.

Family (B: U): U = B -> U

total (B: U) (F: Family B): U = Sigma B F
trivial (B: U) (F: Family B): total B F -> B = \ (x: total B F) -> x.1
homeo (B E: U) (F: Family B) (p: E -> B) (y: B) :
           fiber E B p y -> total B F

Fiber is a Dependent Family

Theorem (Fiber in a trivial total space is a family over base). Inverse image (fiber) of fiber bundle $(F,B*F,pr_1,B)$ in point $y:B$ equals $F(y)$. Thre proof sketch is following:

F y = (_: isContr B) * (F y)
    = (x y: B) * (_: Path B x y) * (F y)
    = (z: B) * (k: F z) * Path B z y
    = (z: E) * Path B z.1 y
    = fiber (total B F) B (trivial B F) y

The equality is proven by $isoPath$ lemma and $encode/decode$ functions.

encode (B: U) (F: B -> U) (y: B)
     : fiber (total B F) B (trivial B F) y -> F y
     = \ (x: fiber (total B F) B (trivial B F) y)
      -> subst B F x.1.1 y (<i>[email protected]) x.1.2

decode (B: U) (F: B -> U) (y: B)
     : F y -> fiber (total B F) B (trivial B F) y
     = \ (x: F y) -> ((y,x),refl B y)

lem2 (B: U) (F: B -> U) (y: B) (x: F y)
   : Path (F y) (comp (<_> F y) x []) x
   = <j> comp (<_> F y) x [ (j=1) -> <_> x]

lem3 (B: U) (F: B -> U) (y: B) (x: fiber (total B F) B (trivial B F) y)
   : Path (fiber (total B F) B (trivial B F) y) ((y,encode B F y x),refl B y) x
   = <i> ((x.2 @ -i,comp (<j> F (x.2 @ -i /\ j)) x.1.2 [(i=1) -> <_> x.1.2 ]),<j> x.2 @ -i \/ j)

TrivialFiberBundleEqualsPi (B: U) (F: Family B) (y: B)
    : Path U (fiber (total B F) B (trivial B F) y) (F y)
    = isoPath T A f g s t where
    T: U = fiber (total B F) B (trivial B F) y
    A: U = F y
    f: T -> A = encode B F y
    g: A -> T = decode B F y
    s (x: A): Path A (f (g x)) x = lem2 B F y x
    t (x: T): Path T (g (f x)) x = lem3 B F y x

G-structure

The structure group of an $F$-fiber bundle is just Aut(F), the loop space of BAut(F).