A characteristic $p$ analog of formal lifting properties

A field extension $L/K$ of characteristic $p > 0$ is formally \'etale if and only if the relative Frobenius of $L/K$ is an isomorphism. Inspired by this classical result, we explore whether the formally \'etale property for a map $R \to S$ of $\mathbf{F}_p$-algebras is characterized by isomorphism of the relative Frobenius $F_{S/R}$. While $F_{S/R}$ being an isomorphism implies $R \to S$ is formally \'etale, the converse fails in the non-Noetherian setting. Thus, following Morrow, we introduce an enhancement of the formally \'etale property that we call b-nil (bounded nil) formally \'etale, and we show that $F_{S/R}$ is an isomorphism precisely when $R \to S$ is b-nil formally \'etale. We prove this result by first establishing several structural properties of b-nil formally smooth maps, which are defined analogously to the formally smooth case. Our structural results reveal that the b-nil formally smooth (resp. \'etale) property is quite different from the formally smooth (resp. \'etale) property. For instance, we show that any b-nil formally smooth algebra over an $F$-pure ring is reduced, whereas non-reduced formally \'etale algebras exist over $\mathbf{F}_p$ by a construction of Bhatt. We also show that the b-nil formally \'etale property neither implies nor is implied by having a trivial cotangent complex. We explore when formally smooth (resp. \'etale) implies b-nil formally smooth (resp. \'etale) in prime characteristic. A satisfactory picture emerges for ideal adic completions.