{- Fiber Bundle: https://groupoid.space/mltt/types/bundle/ - Fiber Bundle; - Trivial Fiber Bundle, Trivial = Pi; - Local F-Bundle (4 definitions). Copyright (c) Groupoid Infinity, 2014-2018. -} module bundle where import iso import infinitesimal import pullback import trunc -- Fiber Bundle -- A fiber bundle p : E -> B is required to be locally trivial, -- which might be witnessed by a pullback square like this: -- V × F ------> E -- |_| | -- v*p | (pb) | p -- | | -- v v -- V ---v--> B -- NOTE: there is twisted hidden structure in p -- U = neighborhood in base B -- fibers locally behave like a products, but could be twisted -- h -- | -- p-inv (V) -> V * F -- | / -- p --| /-- pi1 -- v / -- V -- -- pr_1 o h = p -- F_B -> E -> B -- fiber bundle (F_B,E,p,B), -- F: B -> U -- fiber, ex. Vector Space, Section Space, Dependent Product -- E -- total topological space -- B -- base space -- h: F -> E -- homeomorphism -- p: E -> B -- surjective projection map -- p^-1: B -> E -- section (y: B) = (x: E) * p (x) = y -- E=(y:B)*p^-1 y -- total space -- p^-1 = F -- fiber is iso F_B -- T. E = B * F_B -- fiber bundle called trivial if total space is a cartesian product Family (B: U): U = B -> U Fibration (B: U): U = (X: U) * (X -> B) -- Trivial Fiber Bundle (F,B*F,pi1,B) equals Dependent Family F:B->U -- -- Agda Syntax: -- https://paolocapriotti.com/blog/2013/02/20/families-and-fibrations/ -- -- F y = fiber (total B F) B (trivial B F) y -- = (z: E) * Path B z.1 y -- = (z: B) * (k: F z) * Path B z y -- = (x y: B) * (_: Path B x y) * (F y) -- = (_: isContr B) * (F y) -- = F y fiber (A B: U) (f: A -> B) (y: B): U = (x: A) * Path B (f x) y encode (B: U) (F: B -> U) (y: B) : fiber (Sigma B F) B (pi1 B F) y -> F y = \ (x: fiber (Sigma B F) B (pi1 B F) y) -> subst B F x.1.1 y x.2 x.1.2 decode (B: U) (F: B -> U) (y: B) : F y -> fiber (Sigma B F) B (pi1 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 (refl B y @ i)) x []) x = comp (F (refl B y @ j/\i)) x [(j=1) -> x] lem3 (B: U) (F: B -> U) (y: B) (x: fiber (Sigma B F) B (pi1 B F) y) : Path (fiber (Sigma B F) B (pi1 B F) y) ((y,encode B F y x),refl B y) x = ((x.2 @ -i,comp ( F (x.2 @ -i /\ j)) x.1.2 [(i=1) -> <_> x.1.2 ]), x.2 @ -i \/ j) TrivialEqualsPi (B: U) (F: B -> U) (y: B) : Path U (fiber (Sigma B F) B (pi1 B F) y) (F y) = isoPath T A f g s t where T: U = fiber (Sigma B F) B (pi1 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 -- Local F-Bundle -- Definition (1) Dependent isFBundle1 (B: U) (p: B -> U) (F: U): U = (_: (b: B) -> isContr (Path U (p b) F)) * ((x: Sigma B p) -> B) -- Definition (2) Dependent isFBundle2 (B: U) (p: B -> U) (F: U): U = (V: U) * (v: surjective V B) * ((x: V) -> Path U (p (v.1 x)) F) -- Definition (3) Non-Dependent im1 (A B: U) (f: A -> B): U = (b: B) * pTrunc ((a:A) * Path B (f a) b) BAut (F: U): U = im1 unit U (\(x: unit) -> F) unitIm1 (A B: U) (f: A -> B): im1 A B f -> B = \(x: im1 A B f) -> x.1 unitBAut (F: U): BAut F -> U = unitIm1 unit U (\(x: unit) -> F) isFBundle3 (E B: U) (p: E -> B) (F: U): U = (X: B -> BAut F) * (classify B (BAut F) (\(b: B) -> fiber E B p b) (unitBAut F) X) where classify (A' A: U) (E': A' -> U) (E: A -> U) (f: A' -> A): U = (x: A') -> Path U (E'(x)) (E(f(x))) -- Definition (4) Non-Dependent isFBundle4 (E B: U) (p: E -> B) (F: U): U = (V: U) * (v: surjective V B) * (v': prod V F -> E) * pullbackSq (prod V F) E V B p v.1 v' (\(x: prod V F) -> x.1) -- Theorem 4.3.7 unifamOverBAut (F: U): U = (x: BAut F) * U FBundle (E B: U) (p: E -> B) (F: U) (x: isFBundle3 E B p F) (b: B) : pullbackSq E B (unifamOverBAut F) (BAut F) x.1 (\(x: unifamOverBAut F) -> x.1) p (\(y: E) -> (x.1 (p y),F)) = undefined -- Formal Disk Bundle isInfinitesimalClose (X: U) (a x': X): U = Path (Im X) (ImUnit X a) (ImUnit X x') formalDisc (X: U) (a: X): U = (x': X) * isInfinitesimalClose X a x' unitDisc (X: U) (x: Im X): U = (x': X) * Path (Im X) x (ImUnit X x') starDisc (X: U) (x: X): formalDisc X x = (x, refl (Im X) (ImUnit X x)) differential (X Y: U) (f: X -> Y) (x: X) : formalDisc X x -> formalDisc Y (f x) = undefined formalDiscBundle (A: U): U = (a: A) * formalDisc A a -- T_\infty(A) := \Sigma_{a:A}\mathbb{D}_a lemma45 (A B C: U) (f: A -> B) (g: B -> C) (x: A) : Path (formalDisc A x -> formalDisc C ((o A B C g f) x)) (differential A C (o A B C g f) x) (o (formalDisc A x) (formalDisc B (f x)) (formalDisc C ((o A B C g f) x)) (differential B C g (f x)) (differential A B f x)) = undefined preservesInifinitesimalProximity (X Y: U) (x x': X) (f: X -> Y) : isInfinitesimalClose X x x' -> isInfinitesimalClose Y (f x) (f x') = undefined -- Homogeneous Structure on A = (A) homogeneous (A: U): U = (e: A) * (translationsFamily: (x: A) -> Path U A A) -- could be non-trivial * ((x: A) -> Path A (transport (translationsFamily x) e) x)