Trivial Generic Formal Fiber

A Noetherian local domain A has trivial generic formal fiber if every prime of its adic completion contracting to zero is itself zero. This is the key condition in Jensen's construction of UFDs with prescribed completions.

def HasTrivialGenericFormalFiber (R : Type u_1) [CommRing R] [IsLocalRing R] : Prop

A local ring R has trivial generic formal fiber if every prime ideal of its M-adic completion that contracts to 0 in R is itself 0. (This is the relevant condition for Noetherian local domains.)

Equations

• One or more equations did not get rendered due to their size.