Skip to content

Instantly share code, notes, and snippets.

@andrejbauer andrejbauer/algebraic.v

Last active Jan 15, 2020
Embed
What would you like to do?
Unions of algebraic sets are algebraic
(* 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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.