The abelian fundamental group with modulus in mixed characteristic

We define the abelian fundamental group with modulus of a regular flat scheme over a discrete valuation ring, taking into account wild ramification along a divisor. Our definition provides a mixed-characteristic analogue of the abelian fundamental group with modulus introduced by Kerz--Saito for smooth schemes over a perfect field. In this setting, we prove a Lefschetz-type theorem for strictly semi-stable schemes: restriction to a hypersurface of sufficiently large degree relative to the ramification induces an isomorphism of the abelian fundamental groups.