Applications of Monadicity theorems Crossposted to MO.

Having carefully read the proof of Beck's monadicity theorems and some related variations, I'm now hungry for cool applications.
For instance, I found these blackboard pictures of a lecture by David Jordan, but I do not understand any of the examples - too terse for me.
What are some interesting applications of monadicity theorems, especially in geometric contexts (algebraic geometry would be especially cool)? Can anyone spell out the example(s) presented in the linked pictures?
Added. I know about monadic descent and am trying to slowly understand it. I am hoping for additional examples.
 A: My favorite application is the generalization to semi-abelian categories of the fact that for every short exact sequence
$$\require{AMScd}\begin{CD} 0 @>>>K@>{k}>> A@>{p}>>B @>>>0\end{CD}\tag{1}\label{1} $$
such that $p$ is a split epimorphism, $A$ is isomorphic to $B\ltimes_\xi K$. To obtain this generalization, we need to define actions and semi-direct products in a semi-abelian category $\mathcal{C}$ first, and this is done by constructing a monad on $\mathcal{C}$. All this is done in the paper "Internal objects actions", by Francis Borceux, George Janelidze and Max Kelly.
Let me first recall the definition of semi-abelian category : a category $\mathcal{C}$ is said to be semi-abelian if


*

*it is pointed

*it is Barr-exact

*it is protomodular, which in this context is equivalent to the validity of the (split) Short Five Lemma

*it has binary coproducts.


Now let me first define the category $Pt(B)$ of points over an object $B$ of $\mathcal{C}$. Its objects are the triples $(A,p,s)$ where $A$ is an object of $\mathcal{C}$ and $p:A\to B$ and $s:B\to A$ are such that $ps=1_B$, and a morphism $(A,p,s)\to (A',p',s')$ is a morphism $f:A\to A'$ such that $p'f=p$ and $fs=s'$.
Define moreover two functors :


*

*the kernel functor $Ker:Pt(B)\to \mathcal{C}$ maps an object $(A,p,s)$ to $Ker(p)$ and a morphism $f:(A,p,s)\to (A',p',s')$ to its restriction to the kernels (which is well defined since $p'f=p$).

*the functor $B+\_$ maps an object $X$ to $(B+X,[1_B,0],i_B)$, where $i_B$ is the canonical injection $B\to B+X$, and $[1_B,0]:B+X\to B$ is the arrow induced by the identiy $1_B:B\to B$ and the zero map $0:X\to B$, and maps $f:X\to X'$ to $1_B+f:B+X\to B+X'$.


These functors form an adjunction $B+\_ \dashv Ker$, and the resulting monad is denoted $B\flat\_ $. Since we need to know the unit and counit, I will explain a little bit how it works : an arrow $(B+X,[1_B,0],i_B)\to (A,p,s)$ in $Pt(B)$ is an arrow $f:B+X\to A$ and thus it is determined by $fi_B$ and $fi_X$. But the definition of $Pt(B)$ implies that $fi_B=s$ and $pfi_X=[1_B,0]i_X=0$, so $fi_X$ is determined by its factorisation $\hat{f}X\to Ker (p)$. With this reasoning, we find that the $X$-component of the unit of this adjunction is the factorisation $X\to B\flat X=Ker([1_B,0]:B+X\to B)$ of $i_X:X\to B+X$, and the $(A,p,s)$-component of the counit is $[s,\ker (p)]:B+Ker(p)\to A$.
Now an action of $B$ on $X$ in $\mathcal{C}$ is simply a $B\flat\_$-algebra structure on $X$, i.e. a map $\xi : B\flat X\to X$. This already tells you how to define, for a split short exact sequence \eqref{1}, an action of $B$ on $Ker(p)$: it suffices to apply the comparison functor $Pt(B)\to \mathcal{C}^{B\flat\_}$, which in this case amounts to taking the restriction to $K$ of $[s,k]:B+K\to A$. Now we still need to define semi-direct products; for this, we use the left adjoint to the comparison functor. In general, this left adjoint is obtained for a $T$-algebra $(X,h)$ by taking the coequalizer of $F(h)$ and $\epsilon_{FX}$; in this case, given an action $\xi :B\flat X\to X$, the semi-direct product is thus obtained as the coequalizer of $1_B+\xi $ and $[i_B,\kappa_{B,X}]:B+B\flat X\to B+X$. Note that the comparison functor is defined on $Pt(B)$, so we have to take the coequaliser in $Pt(B)$, but this is just a coequalizer in $\mathcal{C}$. Thus the semi-direct product has a projection $\pi_B:B\ltimes_\xi X\to X$, which has a section $s_B:B\to B\ltimes_\xi X$.
Now the monadicity of the adjunction $B+\_ \dashv Ker$ (which I will prove after this) tells you exactly that for every split epimorphism $p:A\to B$, $(A,p,s)$ is isomorphic to $(B\ltimes_\xi Ker(p),\pi_B,s_B)$, and for every action $\xi : B\flat X\to X$, $Ker(\pi_B)=X$. In other words, every short exact sequence \eqref{1} with $p$ split is isomorphic to one of the form
$$\require{AMScd}\begin{CD} 0 @>>>K@>{}>> B\ltimes K@>{\pi_B}>>B @>>>0.\end{CD} $$
Now why exactly is the adjunction $B+\_ \dashv Ker$ monadic? By (a variant of) Beck's Monadicity theorem, it suffices to check that $Pt(B)$ has coequalizers of reflexive pairs, and that the functor $Ker$ preserves them and reflects isomorphisms. But it's easy to show that $Pt(B)$ has coequalizers of reflexive pairs if $\mathcal{C}$ does, and this is true if $\mathcal{C}$ is semi-abelian : indeed, given a pair of arrows $u_1,u_2:X\to Y$ with a common section in $\mathcal{C}$, then you can take the image of $(u_1,u_2):X\to Y\times Y$, since $\mathcal{C}$ is regular. This defines a relation on $Y$, which is reflective since $u_1$ and $u_2$ have a common section. Now $\mathcal{C}$ is protomodular, and thus also a Mal'tsev category, thus this relation is an equivalence relation, and by exactness it is thus a kernel pair; thus it has a coequalizer, which is then also a coequalizer of $u_1$ and $u_2$. The functor $Ker$ preserves kernel pairs (as any adjoint), but also regular epimorphisms, because these are stable under pullbacks in $\mathcal{C}$, and thus it preserves the construction given above of the coequalizer of a reflexive pair. Lastly, it reflects isomorphisms by protomodularity (as mentioned above).
