∞-Lie theory (higher geometry)
The notion of Ehresmann connection is one of the various equivalent definitions of connection on a bundle.
Let $G$ be a Lie group with Lie algebra $\mathfrak{g}$ and $P \to X$ a $G$-principal bundle. Let
be the action of $G$ on $P$ and
its derivative, sending each element $x \in \mathfrak{g}$ to the vector field on $P$ that at $p \in P$ is the push-forward $\rho(p,-)_*(x)$.
For $v \in \Gamma(T X)$ and $\omega$ a differential form on $P$ write $\iota_v \omega$ for the contraction.
A Cartan-Ehresmann connection on $P$ is a Lie algebra-valued 1-form
on $P$ satisfying two conditions
first Ehresmann condition
for every $x \in \mathfrak{g}$ we have
second Ehresmann condition
for every $x \in \mathfrak{g}$ we have
where $\mathcal{L}_{\rho_*(x)}$ is the Lie derivative along $\rho_*(x)$ and where $ad_x : \mathfrak{g} \to \mathfrak{g}$ is the adjoint action of $\mathfrak{g}$ on itself.
This is equivalent to
first Ehresmann condition
for every $x \in \mathfrak{g}$ we have
second Ehresmann condition
for every $x \in \mathfrak{g}$ we have
where $F_A \in \Omega^2(P, \mathfrak{g})$ is the curvature 2-form of $A$.
Using $\iota_x A = x$ we have by Cartan calculus
Given a smooth bundle $\pi: E\to X$ with typical fiber $F$ (e.g. a smooth vector bundle or a smooth principal $G$-bundle), there is a well defined vector subbundle $V E\subset T E$ over $E$ such that $V_p$ consists of the tangent vectors $v_p$ such that $(T_p \pi)(v_p) = 0$. A smooth distribution (field) of horizontal subspaces is a choice of a vector subspace $H_p E\subset T_p E$ for every $p$ such that
E1. (complementarity) $T_u E \: = \: H_u E \oplus V_u E$
E2. $p\mapsto H_p E$ is smooth. That means that in the unique decomposition of any smooth vector field $X$ on $E$ into vector fields $X^H \in \Gamma(H_u E)$ and $X^V \in \Gamma(V_u E)$ such that $X = X^H + X^V$ the vector field $X^H$ is smooth (or equivalently $X^V$ is smooth, or equivalently both) as a section of $T E$ (there exist yet several other equivalent formulations of the smooothness criterion).
An Ehresmann connection describes a connection on a $G$-principal bundle $\pi : P \to X$ (for $G$ some Lie group) in terms of a distribution of horizontal subspaces $H \subset T P$ which is a subbundle of the tangent bundle of $P$ complementary at each point to the vertical tangent bundle to the fiber. More precisely, an Ehresmann connection on a principal $G$-bundle $\pi:P\to X$ is a smooth distribution of horizontal subspaces $p\mapsto H_p P$ which is equivariant:
E3. $H_{p g}P = (T_p R_g) H_p P$ for every $p \in P$ and $g \in G$.
This subbundle $H = \cup_p H_p\subset T X$ over $X$ can be expressed as a field of subspaces $H_x = Ker A_x = Ann A_x\subset T P$ ($x\in P$) which are pointwise annihilators of a smooth Lie algebra-valued $1$-form $A \in \Omega^1(P,Lie(G))$ on $P$ that satisfies two Ehresmann conditions from the previous subsection.
The Ehresmann connections on a principal $G$-bundle are in 1-1 correspondence with an appropriate notion of a connection on the associated bundle. Namely, if $T^H P\subset T P$ is the smooth horizontal distrubution of subspaces defining the principal connection on a principal $G$-bundle $P$ over $X$, where $G$ is a Lie group and $F$ a smooth left $G$-space, then consider the total space $P\times_G F$ of the associated bundle with typical fiber $F$. Then, for a fixed $f\in F$ one defines a map $\rho_f : P\to P\times_G F$ assigning the class $[p,f]$ to $p\in P$. If $(T_p \rho_f)(T^H_p P) =: T_{[p,f]}^H P\times_G F$ defines the horizontal subspace $T_{[p,f]}^H P\times_G F\subset T_{[p,f]} P\times_G F$, the collection of such subspaces does not depend on the choice of $(p,f)$ in the class $[p,f]$, and the correspondence $p\mapsto T_{[p,f]}^H P\times_G F$ is a connection on the associated bundle $P\times_G F\to X$.
One may also describe(flat) Ehresmann connections in cohesive homotopy type theory.
The general abstract discussion is here. The discussion of how in smooth infinity-groupoids this reduces to the traditional notion is here.
The two definitions in terms of 1-forms and in terms of horizontal distributions are equivalent.
At each $p \in P$ take the horizontal subspace $H_p P$ to be the kernel of $A(p) : T_p P \to \mathfrak{g}$
This means we may think of $A$ as measuring how infinitesimal paths in $P$ fail to be horizontal or parallel to $X$ in the sense of parallel transport.
Let $\langle - \rangle \in W(\mathfrak{g})$ be an invariant polynomial on the Lie algebra. For $A \in Omega^1(P,\mathfrak{g})$ an Ehresmann connection, write
for the curvature characteristic form obtained by evaluating this on wedge powers of the curvature 2-form.
The forms $\langle F_A \rangle \in \Omega^{2k}(P)$ are closed, descend along $p : P \to X$, in that they are pullbacks of forms along $p$, and their class in de Rham cohomology $H^{2k}(X)$ are independent of the choice of $A$ on $P$.
That the forms are closed follows from the Bianchi identity
satisfied by the curvature 2-form and the defining as-invariance of $\langle-\rangle$. More abstractly, the 1-form $A$ itself may be identified with a morphism of dg-algebras out of the Weil algebra $W(\mathfrak{g})$ (see there)
and the evaluation of the curvature in the invariant polynomials corresponds to the precomposition with the morphism
described at ∞-Lie algebra cohomology.
to show that these forms descend, it is sufficient to show that for all $x \in \mathfrak{g}$ we have
$\iota_{\rho_*(X)} \langle F_A \rangle = 0$
$\mathcal{L}_{\rho_*(x)} \langle F_A \rangle = 0$
The first follows from $\iota_{\rho_*(x)} F_A = 0$. The second from this, the $d_{dR}$-closure just discussed and Cartan's magic formula for the Lie derivative.
The form $\langle F_A \rangle$ is called the curvature characteristic form of the connection $A$. The map
induced by $(P,A)$ as above is the Chern-Weil homomorphism.
The terminology for the various incarnations of the single notion of connection on a bundle varies throughout the literature. What we here call an Ehresmann connection is sometimes, but not always, called principal connection (as it is defined for principal bundles).
The original definition is due to
See also
A formulation and discussion of Ehresmann connections using language and tools from synthetic differential geometry is in section 6 of