Locally principal subvariety (source code)

= Locally principal subvariety

A proper subvariety locally defined by one non-zero-divisor is an <effective Cartier divisor>. On an integral <variety> a nonzero local equation is automatically a <non-zero-divisor>. Its <conormal sheaf> is a <line bundle>, since $A/(f)\cong(f)/(f^2)$ via multiplication by $f$. Allowing the zero equation would include the whole <variety> and would not give this conclusion.