How to formalize a statement about projective subschemes

Stream: new members

[Xipan Xiao]

Trying to formalize the following statement:

(Hypersurfaces meet everything of dimension at least 1 in projective space, unlike in affine space.) Suppose X is a closed subset of P^n_k of dimension at least 1, and H is a nonempty hypersurface in P^n_k. Show that H meets X.

I was told that formalization of projective schemes is not available in mathlib4 yet. Is this true? And if there any replacement/workaround I can take? For example, an algebraic version of this statement whose formalization is in mathlib4. Thanks.

[Kenny Lau]

@Xipan Xiao We have Proj, but I do want to work on P^n at some point.

[Paul Lezeau]

Kenny Lau said:

Xipan Xiao We have Proj, but I do want to work on P^n at some point.

I have a definition of $\mathbb{P}^n$ here which I could upstream at some point.