Unions of algebraic sets are algebraic

algebraic.v

(* A Coq formalization of the theorem that the the union of algebraic sets are algebraic.

   The file is self-contained, so we start with some general definitions
   and facts from logic and sets, and basic algebraic definitions.
   It should be straight-forward to translate it to any setting that has
   a decent library of basic facts of logic, set theory and algebra.
*)

(* We formalize the following "paper" proof.

Consider a field F and let X be a finite-dimensional vector space over F.
Given a set U ⊆ (X → F) of maps from X to F, define the zero-set of U to be

  Z(U) = { x ∈ X | ∀ s ∈ U , s x = 0 }.

Given sets U, V ⊆ (X → F), define

  U · V = { s · t : X → F | s ∈ U, t ∈ V }

We claim that

  Z(U) ∪ Z(V) = Z(U · V)

Indeed, we have the following chain of equivalences:

  x ∈ Z(U) ∪ Z(V)

  ⇔ [definition of ∪]

  x ∈ Z(U) ∨ x ∈ Z(V)

  ⇔ [definition of Z]

  (∀ s ∈ U. s x = 0) ∨ (∀ t ∈ V . t x = 0)

  ⇔ [by a basic fact of logic]

  ∀ s ∈ U. ∀ t ∈ V . s x = 0 ∨ t x = 0

  ⇔ [because F does not have zero divisors]

  ∀ s ∈ U. ∀ t ∈ V . s x * t x = 0

  ⇔ [definition of s · t]

  ∀ s ∈ U. ∀ t ∈ V . (s · t) x = 0

  ⇔ [by a basic fact of logic and definition of U · V]

  ∀ f ∈ U · V . f x = 0

  ⇔ [definition of Z]

  x ∈ Z(U · V)

QED
*)

(* Everything from here up to the main theorem union_Z at the bottom is provided just so that the file
   is self-sufficient. Any respectable library of formalized mathematics should allow us to
   directly formalize union_Z, possibly with the help of the lemma Z_prod. *) 
   
(**** Logical preliminaries ****)

(* We assume excluded middle *)
Axiom lem : forall p : Prop, p \/ ~ p.

(* Reductio ad absurdum follows from excluded middle. *)
Lemma raa: forall p : Prop, ~ ~ p -> p.
Proof.
  intro p.
  destruct (lem p); tauto.
Qed.

(* Excluded middle implies that a disjunction can be expressed as an implication. *)
Lemma or_impl p q : p \/ q <-> (~p -> q).
Proof.
  destruct (lem p) ; tauto.
Qed.

(**** Set-theoretic preliminaries ****)

(* The powerset of X is written as P X. *)
Definition P (X : Type) := X -> Prop.
Definition element {X} (x : X) (S : P X) := S x.

(* Some convenient set-theoretic notations. *)
Notation "x '∈' S" := (element x S) (at level 70).
Notation "'all' x '∈' S ',' p" := (forall x, x ∈ S -> p) (at level 100, x at level 69, p at level 100).
Notation "'some' x '∈' S ',' p" := (exists x, x ∈ S /\ p) (at level 100, x at level 69, p at level 100).
Notation "'{' x ';' p '}'" := (fun x => p).

(* Union of subsets. *)
Definition union {X} (S T : P X) := { x ; x ∈ S \/ x ∈ T }.
Notation "S '∪' T" := (union S T) (at level 60).

(* Excluded middle implies that a negated ∀ gives an ∃. *)
Theorem not_all_some {X} (S : P X) (p : X -> Prop) :
  ~ (all x ∈ S, p x) -> some x ∈ S, ~ p x.
Proof.
  intro not_allx.
  apply raa.
  intro not_somex.
  absurd (all x ∈ S, p x) ; auto.
  intros x x_in_S.
  apply raa.
  intro not_px.
  absurd (some x ∈ S, ~ p x) ; auto.
  now exists x.
Qed.

(* Excluded middle also implies that ∀ and ∨ can be factored as follows. *)
Theorem all_or X (U V : P X) (p q : X -> Prop) :
  (all x ∈ U, all y ∈ V, p x \/ p y) <-> (all x ∈ U, p x) \/ (all y ∈ V, p y).
Proof.
  split.
  - intro all_xy.
    apply or_impl.
    intro H.
    destruct (not_all_some _ _ H) as [x [x_in_U not_px]].
    intros y y_in_V.
    now destruct (all_xy x x_in_U y y_in_V).
  - intros allx_or_ally x x_in_U y y_in_V.
    destruct allx_or_ally as [H | H].
    + left. now apply H.
    + right. now apply H.
Qed.

(**** Algebraic preliminaries ****)

(* We define only as much of algebra as is needed to express the proof. *)

(* We consider a field F. We only need to know that F has multiplication and 0. *)
Parameter F : Type.
Parameter zero : F.
Notation "0" := zero.

Parameter mult : F -> F -> F.
Notation "x '*' y" := (mult x y).

(* Zero absorbs multiplication *)
Parameter mult_0_left : forall x y, x = 0 -> x * y = 0.
Parameter mult_0_right: forall x y, y = 0 -> x * y = 0.

(* There are no zero divisors in a field. *)
Parameter zero_divisors: forall x y, x * y = 0 -> x = 0 \/ y = 0.

(* Usually algebraic sets are defined as subsets of a vector space over F, but
   really, we can just work with any set X. Just imagine that X is a finite-dimensional
   vector space over F. *)
Parameter X : Type.

(* The zero-set of a set of maps X -> F. *)
Definition Z (U : P (X -> F)) := { x ; all s ∈ U, s x = 0 }.

(* Given two sets U and V of maps X -> F, prod U V is the set of all maps s * t where s ∈ U and t ∈ V. *)
Definition prod (U V : P (X -> F)) :=
  { f ; some s ∈ U, some t ∈ V, forall x, f x = s x * t x }.

(* Everything up to here should be considered as prelimnaries. *)

(* Convenience lemma, characterizing the zero-set of prod U V *)
Lemma Z_prod U V x :
  x ∈ Z (prod U V) <-> all s ∈ U, all t ∈ V, s x * t x = 0.
Proof.
  split.
  - intros x_in_Zprod s s_in_U t t_in_V.
    pose (f := fun x => s x * t x).
    transitivity (f x) ; auto.
    apply x_in_Zprod.
    exists s. split ; auto.
    exists t. split ; auto.
  - intros st_0 f [s [s_in_U [t [t_in_V f_is_st]]]].
    rewrite f_is_st.
    now apply st_0.
Qed.

(* Main theorem. *)
Theorem union_Z (U V : P (X -> F)) :
  forall x, x ∈ (Z U) ∪ (Z V) <-> x ∈ Z (prod U V).
Proof.
  (* consider any x ∈ X *)
  intro x.
  (* split <-> into -> and <- *)
  split.
  - intros x_in_ZU_u_ZV f [s [s_in_U [t [t_in_V f_is_st]]]].
    rewrite f_is_st.
    destruct x_in_ZU_u_ZV as [x_in_ZU | x_in_ZV].
    + now apply mult_0_left, x_in_ZU.
    + now apply mult_0_right, x_in_ZV.
  - intros x_in_ZprodUV.
    cut (x ∈ Z U \/ x ∈ Z V) ; auto.
    apply (all_or _ U V (fun s => s x = 0) (fun s => s x = 0)).
    intros s s_in_U t t_in_V.
    apply zero_divisors.
    now apply (Z_prod U V).
Qed.