Cómo entender un haz principal en la teoría de tipos de homotopía

Question

En la Teoría de Yang-Mills, el campo que interactúa es capturado por un haz principal $P$ . En particular, sea G el grupo que es homeomorfo a las fibras que preserva al actuar sobre ellas. Para las fibras $P(x)$ y $P(y)$ de $P$ y $g$ un elemento de $G$ que actúa sobre ellos, es $p(x)g=p(y)$ Por lo tanto $p(x)\sim p(y)$ .

Quiero traducir lo anterior en HoTT. Supongo que hay un camino $\gamma$ entre x e y y en HoTT, esto significa que hay un tipo de identidad $\gamma: x=_U y$ . En primer lugar, se observa que el campo interactivo se expresa mediante la función de tipo dependiente $\varepsilon:\prod_{(x: U)} P(x)$ para un poco de espacio $U$ . Aunque los elementos $p(x):P(x)$ y $p(y):P(y)$ pertenecen a tipos distintos y, por tanto, no está definida una relación de identidad entre ellos, se puede establecer entre ellos un morfismo que es una relación de equivalencia, es decir, existe una función $ f: P(x) \rightarrow P(y)$ . Topológicamente, el tipo de función puede ser tratado por un levantamiento de trayectoria en una fibración donde $U$ constituye el espacio base, $P(x)$ es la fibra sobre x y $\sum_{(x:U)} P(x)$ es el espacio total, donde en lógica esto se traduce como la existencia de tal espacio de fibras. Elevar un camino al espacio total, significa que existe un tipo de identidad $lift: (x, p(x))=(y, f(p(x))$ en el espacio total. Por lo tanto, no existe una relación de identidad $p(x)=p(y)$ aunque existe un tipo de identidad $x=_Uy$ .

Ahora, cuando G actúa sobre las fibras, sospecho que esto significa que hay una función $g: p(x) \rightarrow p(y)$ o hay un tipo de identidad $lift: (x, p(x))=(y, g(p(x))$ . Por otro lado, con respecto al grupo de automorfismo, para $p(x), q(x):P(x)$ hay un tipo de identidad en el espacio total $\sum_{(x:U_i)} P(x)$ para que $g, g': p(x)=_{P(x)}q(x)$ .

Mi pregunta es dónde exactamente estoy cometiendo el error en lo anterior y en particular, no estoy seguro de que $(x, p(x))=(y, g(p(x))$ cuando g actúa sobre las fibras, más bien al igual que presenté el caso del automorfismo, puede ser que $g$ es un morfismo/camino en una relación de identidad (entre p(x) y p(y) (???)).

Espero no haber cometido ningún error en las anotaciones.

Answer 1

Se podría intentar emular ingenuamente la definición habitual. A saber, se podría exigir una acción (continua) de su grupo estructural (topológico) $G$ en su espacio total $\sum_{x:B}P(x)$ , es decir, un término $\phi$ de tipo

$$\sum_{x:B}P(x) \times G \rightarrow \sum_{x:B}P(x)$$

o su currificación, es decir, un término del tipo

$$\sum_{x:B}P(x) \rightarrow (G \rightarrow \sum_{x:B}P(x))$$

que satisface los axiomas de una acción. También debe exigir que la acción sea libre y transitiva. Por último, la acción debe preservar las fibras. Con esta última condición hay que tener cuidado. En efecto, se puede exigir para todos los elementos $x$ de $B$ , $y$ de $P(x)$ y $g$ de $G$ un elemento del tipo de identidad $pr1 (\phi((x,y),g)) =_{B} x$ , donde $pr1$ denota la primera proyección fuera del espacio total. Pero este tipo de identidad es un grupo superior ¡! Por lo tanto, para eludir esto podría requerir su tipo de base $B$ para ser un conjunto, es decir un tipo de hlevel 2 en este caso el tipo de identidad anterior sería una (mera) proposición . También puede exigir que $P$ es una familia de conjuntos, es decir, para todo $x$ de $B$ el tipo $P(x)$ debe ser un conjunto, en este caso se podría demostrar que su espacio total es un conjunto.

Dicho esto, probablemente no sea el enfoque correcto y he mencionado este ingenuo para mostrar dónde pueden surgir algunos problemas si se imita la definición habitual sin cuidado.

Podría tener más sentido en el contexto de la teoría de tipos de homotopía seguir la definición de haces principales en términos de pullbacks de homotopía.