:: {I}ntroduction to {A}lgebraic {G}eometry
:: by Yasushige Watase
::
:: Received June 30, 2023
:: Copyright (c) 2023-2024 Association of Mizar Users


definition
let n be Ordinal;
let L be non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr ;
let p be Polynomial of n,L;
:: original: {
redefine func {p} -> Subset of (Polynom-Ring (n,L));
coherence
{p} is Subset of (Polynom-Ring (n,L))
proof end;
end;

::$INSERT Enhance eval function: evaluated function is Element of Polynom-Ring.
definition
let n be Ordinal;
let L be non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr ;
let f be Element of (Polynom-Ring (n,L));
let x be Function of n,L;
func E_eval (f,x) -> Element of L means :Def1: :: ALGGEO_1:def 1
 ex p being Polynomial of n,L st
( p = f & it = eval (p,x) );
existence
ex b1 being Element of L ex p being Polynomial of n,L st
( p = f & b1 = eval (p,x) )
proof end;
uniqueness
for b1, b2 being Element of L st ex p being Polynomial of n,L st
( p = f & b1 = eval (p,x) ) & ex p being Polynomial of n,L st
( p = f & b2 = eval (p,x) ) holds
b1 = b2 ;
end;

:: deftheorem Def1 defines E_eval ALGGEO_1:def 1 :
for n being Ordinal
for L being non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr
for f being Element of (Polynom-Ring (n,L))
for x being Function of n,L
for b5 being Element of L holds
( b5 = E_eval (f,x) iff ex p being Polynomial of n,L st
( p = f & b5 = eval (p,x) ) );

::$INSERT Enhance E_eval function to evaluate Finite Sequence of Polynomials.
definition
let n be Ordinal;
let L be non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr ;
let F be FinSequence of the carrier of (Polynom-Ring (n,L));
let x be Function of n,L;
func E_eval (F,x) -> FinSequence of the carrier of L means :Def2: :: ALGGEO_1:def 2
( dom it = dom F & ( for i being Nat st i in dom F holds
it . i = E_eval ((F /. i),x) ) );
existence
ex b1 being FinSequence of the carrier of L st
( dom b1 = dom F & ( for i being Nat st i in dom F holds
b1 . i = E_eval ((F /. i),x) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of the carrier of L st dom b1 = dom F & ( for i being Nat st i in dom F holds
b1 . i = E_eval ((F /. i),x) ) & dom b2 = dom F & ( for i being Nat st i in dom F holds
b2 . i = E_eval ((F /. i),x) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines E_eval ALGGEO_1:def 2 :
for n being Ordinal
for L being non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr
for F being FinSequence of the carrier of (Polynom-Ring (n,L))
for x being Function of n,L
for b5 being FinSequence of the carrier of L holds
( b5 = E_eval (F,x) iff ( dom b5 = dom F & ( for i being Nat st i in dom F holds
b5 . i = E_eval ((F /. i),x) ) ) );

theorem Th1: :: ALGGEO_1:1
for L being non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr
for n being Ordinal holds Support (0_ (n,L)) = {}
proof end;

theorem Th2: :: ALGGEO_1:2
for n being Ordinal
for L being non trivial right_complementable well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for f, g being Element of (Polynom-Ring (n,L))
for x being Function of n,L holds E_eval ((f + g),x) = (E_eval (f,x)) + (E_eval (g,x))
proof end;

theorem Th3: :: ALGGEO_1:3
for n being Ordinal
for L being non empty non trivial right_complementable well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for f, g being Element of (Polynom-Ring (n,L))
for x being Function of n,L holds E_eval ((f * g),x) = (E_eval (f,x)) * (E_eval (g,x))
proof end;

theorem Th4: :: ALGGEO_1:4
for N0 being Nat
for n being Ordinal
for L being non empty non trivial right_complementable well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for F being FinSequence of the carrier of (Polynom-Ring (n,L))
for x being Function of n,L st len F = N0 + 1 holds
E_eval (F,x) = (E_eval ((F | N0),x)) ^ <*(E_eval ((F /. (len F)),x))*>
proof end;

theorem Th5: :: ALGGEO_1:5
for n being Ordinal
for L being non empty non trivial right_complementable well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for F being FinSequence of the carrier of (Polynom-Ring (n,L))
for x being Function of n,L holds E_eval ((Sum F),x) = Sum (E_eval (F,x))
proof end;

Lm1: for R being domRing
for G being FinSequence of the carrier of R holds
( G = (len G) |-> (0. R) iff for i being Nat st i in dom G holds
G . i = 0. R )
proof end;

Lm2: for R being domRing
for n being Nat holds Sum (n |-> (0. R)) = 0. R
proof end;

::$INSERT monic multivariate Polynomials with degree 1.
definition
let n be non empty Ordinal;
let R be domRing;
let a be Function of n,R;
let i be Element of n;
func deg1Poly (a,i) -> Polynomial of n,R equals :: ALGGEO_1:def 3
(1_1 (i,R)) - ((a . i) | (n,R));
coherence
(1_1 (i,R)) - ((a . i) | (n,R)) is Polynomial of n,R ;
end;

:: deftheorem defines deg1Poly ALGGEO_1:def 3 :
for n being non empty Ordinal
for R being domRing
for a being Function of n,R
for i being Element of n holds deg1Poly (a,i) = (1_1 (i,R)) - ((a . i) | (n,R));

theorem Th6: :: ALGGEO_1:6
for R being domRing
for n being non empty Ordinal
for a being Element of R
for i being Element of n holds
( (1_1 (i,R)) . (UnitBag i) = 1. R & (a | (n,R)) . (EmptyBag n) = a & (1_1 (i,R)) . (EmptyBag n) = 0. R & (a | (n,R)) . (UnitBag i) = 0. R )
proof end;

theorem :: ALGGEO_1:7
for R being domRing
for n being non empty Ordinal
for a being Element of R
for i being Element of n holds
( 1_1 (i,R) is Polynomial of n,R & a | (n,R) is Polynomial of n,R ) ;

theorem :: ALGGEO_1:8
for R being domRing
for n being non empty Ordinal
for a being non zero Element of R
for b being Element of R
for i being Element of n holds ((a | (n,R)) *' (1_1 (i,R))) + (b | (n,R)) is Polynomial of n,R ;

theorem Th9: :: ALGGEO_1:9
for R being domRing
for n being non empty Ordinal
for a being Element of R
for i being Element of n holds Support ((1_1 (i,R)) + (a | (n,R))) c= {(UnitBag i)} \/ {(EmptyBag n)}
proof end;

theorem Th10: :: ALGGEO_1:10
for n being non empty Ordinal holds degree (EmptyBag n) = 0
proof end;

theorem Th11: :: ALGGEO_1:11
for n being non empty Ordinal
for x being Element of n holds degree (UnitBag x) = 1
proof end;

theorem :: ALGGEO_1:12
for R being domRing
for n being non empty Ordinal
for a being Element of R
for i being Element of n holds degree ((1_1 (i,R)) + (a | (n,R))) = 1
proof end;

::$INSERT Enhance function Roots for multivariate Polynomials.
definition
let R be domRing;
let n be non empty Ordinal;
let f be Polynomial of n,R;
func Zero_ f -> Subset of (Funcs (n,([#] R))) equals :: ALGGEO_1:def 4
 { x where x is Function of n,R : eval (f,x) = 0. R } ;
coherence
{ x where x is Function of n,R : eval (f,x) = 0. R } is Subset of (Funcs (n,([#] R)))
proof end;
end;

:: deftheorem defines Zero_ ALGGEO_1:def 4 :
for R being domRing
for n being non empty Ordinal
for f being Polynomial of n,R holds Zero_ f = { x where x is Function of n,R : eval (f,x) = 0. R } ;

::NdR Fulton69: p.9 (5): V(0) = A^n(k)
theorem Th13: :: ALGGEO_1:13
for R being domRing
for n being non empty Ordinal holds Zero_ (0_ (n,R)) = Funcs (n,([#] R))
proof end;

::NdR Fulton69: p.9 (5): V(1) = {}.
theorem Th14: :: ALGGEO_1:14
for R being domRing
for n being non empty Ordinal holds Zero_ (1_ (n,R)) = {} (Funcs (n,([#] R)))
proof end;

::1.2 Affine Space and Algebraic Sets
::$INSERT Enhance function Zero_ for set of Polynomials.
definition
let R be domRing;
let n be non empty Ordinal;
let S be Subset of (Polynom-Ring (n,R));
func Zero_ S -> Subset of (Funcs (n,([#] R))) equals :Def6: :: ALGGEO_1:def 5
 { x where x is Function of n,R : for p being Polynomial of n,R st p in S holds
eval (p,x) = 0. R } if S <> {}
otherwise {} ;
coherence
( ( S <> {} implies { x where x is Function of n,R : for p being Polynomial of n,R st p in S holds
eval (p,x) = 0. R } is Subset of (Funcs (n,([#] R))) ) & ( not S <> {} implies {} is Subset of (Funcs (n,([#] R))) ) )
proof end;
consistency
for b1 being Subset of (Funcs (n,([#] R))) holds verum ;
end;

:: deftheorem Def6 defines Zero_ ALGGEO_1:def 5 :
for R being domRing
for n being non empty Ordinal
for S being Subset of (Polynom-Ring (n,R)) holds
( ( S <> {} implies Zero_ S = { x where x is Function of n,R : for p being Polynomial of n,R st p in S holds
eval (p,x) = 0. R } ) & ( not S <> {} implies Zero_ S = {} ) );

theorem Th15: :: ALGGEO_1:15
for R being domRing
for n being non empty Ordinal
for p being Polynomial of n,R holds Zero_ {p} = Zero_ p
proof end;

definition
let R be domRing;
let n be non empty Ordinal;
let IT be Subset of (Funcs (n,([#] R)));
attr IT is algebraic_set_from_ideal means :Def7: :: ALGGEO_1:def 6
 ex I being Ideal of (Polynom-Ring (n,R)) st IT = Zero_ I;
end;

:: deftheorem Def7 defines algebraic_set_from_ideal ALGGEO_1:def 6 :
for R being domRing
for n being non empty Ordinal
for IT being Subset of (Funcs (n,([#] R))) holds
( IT is algebraic_set_from_ideal iff ex I being Ideal of (Polynom-Ring (n,R)) st IT = Zero_ I );

registration
let R be domRing;
let n be non empty Ordinal;
cluster non empty algebraic_set_from_ideal for Element of K10((Funcs (n,([#] R))));
existence
ex b1 being non empty Subset of (Funcs (n,([#] R))) st b1 is algebraic_set_from_ideal
proof end;
end;

::$INSERT Definition of Algebraic Set.
definition
let n be non empty Ordinal;
let R be domRing;
mode Algebraic_Set of n,R is algebraic_set_from_ideal Subset of (Funcs (n,([#] R)));
end;

::NdR Fulton69: p.9 (3): If I c= J then V(J) c= V(I).
theorem Th16: :: ALGGEO_1:16
for R being domRing
for n being non empty Ordinal
for S, T being non empty Subset of (Polynom-Ring (n,R)) st S c= T holds
Zero_ T c= Zero_ S
proof end;

::NdR Fulton69: p.9 (1): If I is the ideal in k[x1,...,xn] generated by S....
theorem Th17: :: ALGGEO_1:17
for R being domRing
for n being non empty Ordinal
for S being non empty Subset of (Polynom-Ring (n,R)) holds Zero_ S = Zero_ (S -Ideal)
proof end;

theorem Th18: :: ALGGEO_1:18
for R being domRing
for n being non empty Ordinal
for I, J being Ideal of (Polynom-Ring (n,R)) holds Zero_ (I \/ J) = (Zero_ I) /\ (Zero_ J)
proof end;

theorem Th19: :: ALGGEO_1:19
for R being domRing
for n being non empty Ordinal
for S, T being Algebraic_Set of n,R holds S /\ T is Algebraic_Set of n,R
proof end;

Lm3: for A being non degenerated comRing
for F being non empty Subset of (Ideals A) holds union F is non empty Subset of A
proof end;

definition
let A be non degenerated comRing;
let F be non empty Subset of (Ideals A);
:: original: union
redefine func union F -> non empty Subset of A;
coherence
union F is non empty Subset of A by Lm3;
end;

::NdR Fulton69: p.9(2):If {Ij} is any collection of ideals then V(\/Ij)=/\V(Ij)
theorem :: ALGGEO_1:20
for R being domRing
for n being non empty Ordinal
for F being non empty Subset of (Ideals (Polynom-Ring (n,R))) holds Zero_ (union F) = meet { (Zero_ I) where I is Ideal of (Polynom-Ring (n,R)) : I in F }
proof end;

::NdR Fulton69:p.9 (4): V(FG) = V(F) \/ V(G)
theorem Th21: :: ALGGEO_1:21
for R being domRing
for n being non empty Ordinal
for f, g being Polynomial of n,R holds Zero_ {(f *' g)} = (Zero_ {f}) \/ (Zero_ {g})
proof end;

theorem Th22: :: ALGGEO_1:22
for R being domRing
for n being non empty Ordinal
for I, J being Ideal of (Polynom-Ring (n,R)) holds Zero_ (I /\ J) = (Zero_ I) \/ (Zero_ J)
proof end;

theorem :: ALGGEO_1:23
for R being domRing
for n being non empty Ordinal
for I, J being Ideal of (Polynom-Ring (n,R)) holds Zero_ (I *' J) = (Zero_ I) \/ (Zero_ J)
proof end;

definition
let n be non empty Ordinal;
let R be domRing;
func Alg_Sets (n,R) -> set equals :: ALGGEO_1:def 7
 { S where S is Subset of (Funcs (n,([#] R))) : S is Algebraic_Set of n,R } ;
coherence
{ S where S is Subset of (Funcs (n,([#] R))) : S is Algebraic_Set of n,R } is set ;
end;

:: deftheorem defines Alg_Sets ALGGEO_1:def 7 :
for n being non empty Ordinal
for R being domRing holds Alg_Sets (n,R) = { S where S is Subset of (Funcs (n,([#] R))) : S is Algebraic_Set of n,R } ;

::NdR Fulton69: p.9 (4)-any finite union of algebraic sets is an algebraic set.
theorem Th24: :: ALGGEO_1:24
for R being domRing
for n being non empty Ordinal
for m being non zero Nat
for F being Subset of (Alg_Sets (n,R)) st card F = m holds
union F is Algebraic_Set of n,R
proof end;

Lm4: for R being domRing
for n being non empty Ordinal holds Zero_ ([#] (Polynom-Ring (n,R))) = {} (Funcs (n,([#] R)))
proof end;

definition
let n be non empty Ordinal;
let R be domRing;
let a be Function of n,R;
func polyset a -> non empty Subset of (Polynom-Ring (n,R)) equals :: ALGGEO_1:def 8
 { f where f is Polynomial of n,R : ex i being Element of n st f = deg1Poly (a,i) } ;
coherence
{ f where f is Polynomial of n,R : ex i being Element of n st f = deg1Poly (a,i) } is non empty Subset of (Polynom-Ring (n,R))
proof end;
end;

:: deftheorem defines polyset ALGGEO_1:def 8 :
for n being non empty Ordinal
for R being domRing
for a being Function of n,R holds polyset a = { f where f is Polynomial of n,R : ex i being Element of n st f = deg1Poly (a,i) } ;

::NdR Fulton69: p.9 (5): V(x_1-a_1,x_2-a_2,...x_n-a_n) = {(a_1,...a_n)}.
theorem Th25: :: ALGGEO_1:25
for R being domRing
for n being non empty Ordinal
for a being Function of n,R holds Zero_ (polyset a) = {a}
proof end;

theorem Th26: :: ALGGEO_1:26
for R being domRing
for n being non empty Ordinal
for x being Element of Funcs (n,([#] R)) holds {x} is Algebraic_Set of n,R
proof end;

::NdR Fulton69: p.9 (5): any finite subset A^n(k) is an algebaic set.
theorem :: ALGGEO_1:27
for R being domRing
for n being non empty Ordinal
for m being non zero Nat
for P being Subset of (singletons (Funcs (n,([#] R)))) st card P = m holds
union P is Algebraic_Set of n,R
proof end;

::$INSERT The Ideal of a Set of Points.
definition
let R be domRing;
let n be non empty Ordinal;
let X be Subset of (Funcs (n,([#] R)));
func Ideal_ X -> non empty Subset of (Polynom-Ring (n,R)) equals :: ALGGEO_1:def 9
 { f where f is Polynomial of n,R : X c= Zero_ f } ;
coherence
{ f where f is Polynomial of n,R : X c= Zero_ f } is non empty Subset of (Polynom-Ring (n,R))
proof end;
end;

:: deftheorem defines Ideal_ ALGGEO_1:def 9 :
for R being domRing
for n being non empty Ordinal
for X being Subset of (Funcs (n,([#] R))) holds Ideal_ X = { f where f is Polynomial of n,R : X c= Zero_ f } ;

Lm5: for R being domRing
for n being non empty Ordinal
for X being Subset of (Funcs (n,([#] R)))
for p, q being Element of (Polynom-Ring (n,R)) st p in Ideal_ X & q in Ideal_ X holds
p + q in Ideal_ X
proof end;

Lm6: for R being domRing
for n being non empty Ordinal
for X being Subset of (Funcs (n,([#] R)))
for a, p being Element of (Polynom-Ring (n,R)) st p in Ideal_ X holds
a * p in Ideal_ X
proof end;

Lm7: for R being domRing
for n being non empty Ordinal
for X being Subset of (Funcs (n,([#] R)))
for a, p being Element of (Polynom-Ring (n,R)) st p in Ideal_ X holds
p * a in Ideal_ X
by Lm6;

theorem :: ALGGEO_1:28
for R being domRing
for n being non empty Ordinal
for X being Subset of (Funcs (n,([#] R))) holds Ideal_ X is Ideal of (Polynom-Ring (n,R))
proof end;

registration
let R be domRing;
let n be non empty Ordinal;
let X be Subset of (Funcs (n,([#] R)));
cluster Ideal_ X -> add-closed for Subset of (Polynom-Ring (n,R));
coherence
for b1 being Subset of (Polynom-Ring (n,R)) st b1 = Ideal_ X holds
b1 is add-closed by Lm5;
cluster Ideal_ X -> right-ideal for Subset of (Polynom-Ring (n,R));
coherence
for b1 being Subset of (Polynom-Ring (n,R)) st b1 = Ideal_ X holds
b1 is right-ideal by Lm7;
end;

::NdR Fulton69: p.11 (6): if X c= Y, then I(Y) c= I(X)
theorem Th29: :: ALGGEO_1:29
for R being domRing
for n being non empty Ordinal
for X, Y being Subset of (Funcs (n,([#] R))) st X c= Y holds
Ideal_ Y c= Ideal_ X
proof end;

::NdR Fulton69: p.11 (7): I({}) = k[x_1,...,x_n]
theorem Th30: :: ALGGEO_1:30
for R being domRing
for n being non empty Ordinal
for X being Subset of (Funcs (n,([#] R))) holds
( X = {} iff Ideal_ X = [#] (Polynom-Ring (n,R)) )
proof end;

::NdR Fulton69: p 11 (7): I(A^n(k)) = (0) (only (0) c= I(A^n(k)))
theorem :: ALGGEO_1:31
for R being domRing
for n being non empty Ordinal holds {(0. (Polynom-Ring (n,R)))} c= Ideal_ ([#] (Funcs (n,([#] R))))
proof end;

::NdR Fulton69: p.11 (8): S c= I(V(S))
theorem Th32: :: ALGGEO_1:32
for R being domRing
for n being non empty Ordinal
for S being Subset of (Polynom-Ring (n,R)) holds S c= Ideal_ (Zero_ S)
proof end;

::NdR Fulton69: p.11 (8): X c= V(I(X))
theorem Th33: :: ALGGEO_1:33
for R being domRing
for n being non empty Ordinal
for X being Subset of (Funcs (n,([#] R))) holds X c= Zero_ (Ideal_ X)
proof end;

::NdR Fulton69: p.11 (9): V(I(V(S))) = V(S)
theorem Th34: :: ALGGEO_1:34
for R being domRing
for n being non empty Ordinal
for S being Subset of (Polynom-Ring (n,R)) holds Zero_ (Ideal_ (Zero_ S)) = Zero_ S
proof end;

::NdR Fulton69: p.11 (9): I(V(I(X))) = I(X)
theorem :: ALGGEO_1:35
for R being domRing
for n being non empty Ordinal
for X being Subset of (Funcs (n,([#] R))) holds Ideal_ (Zero_ (Ideal_ X)) = Ideal_ X by Th32, Th29, Th33;

::NdR Fulton69: p.11 (9): V=V(I(V)) if V is an algebraic set.
theorem Th36: :: ALGGEO_1:36
for R being domRing
for n being non empty Ordinal
for X being Algebraic_Set of n,R holds X = Zero_ (Ideal_ X)
proof end;

theorem :: ALGGEO_1:37
for R being domRing
for n being non empty Ordinal
for V, W being Algebraic_Set of n,R holds
( V = W iff Ideal_ V = Ideal_ W )
proof end;

::NdR Fulton69: p.11 (6): case of strict subset.
theorem Th38: :: ALGGEO_1:38
for R being domRing
for n being non empty Ordinal
for X, Y being Algebraic_Set of n,R st X c< Y holds
Ideal_ Y c< Ideal_ X
proof end;

Lm8: for R being domRing
for n being non empty Ordinal
for p being Polynomial of n,R
for i being non zero Nat holds Zero_ {(p `^ i)} = Zero_ {p}
proof end;

::NdR Fulton69: p.11 (10): I(X) is a radical ideal for any set X c= A^n(k).
theorem :: ALGGEO_1:39
for R being domRing
for n being non empty Ordinal
for X being Subset of (Funcs (n,([#] R))) holds sqrt (Ideal_ X) = Ideal_ X
proof end;

::$INSERT Reducible Algebraic Set.
definition
let R be domRing;
let n be non empty Ordinal;
let IT be Algebraic_Set of n,R;
attr IT is reducible means :: ALGGEO_1:def 10
 ex V1, V2 being Algebraic_Set of n,R st
( IT = V1 \/ V2 & V1 c< IT & V2 c< IT );
end;

:: deftheorem defines reducible ALGGEO_1:def 10 :
for R being domRing
for n being non empty Ordinal
for IT being Algebraic_Set of n,R holds
( IT is reducible iff ex V1, V2 being Algebraic_Set of n,R st
( IT = V1 \/ V2 & V1 c< IT & V2 c< IT ) );

notation
let R be domRing;
let n be non empty Ordinal;
let V be Algebraic_Set of n,R;
antonym irreducible V for reducible ;
end;

::NdR Fulton69:p.15 Prop1. An algebraic set V is irreducible iff I(V) is prime.
theorem :: ALGGEO_1:40
for R being domRing
for n being non empty Ordinal
for V being non empty Algebraic_Set of n,R holds
( V is irreducible iff Ideal_ V is prime Ideal of (Polynom-Ring (n,R)) )
proof end;