proposition: Lemma zariski_topology_and : isSetOfOpen_and zariski_topology.
proof: Proof. unfold zariski_topology. intros U V HU HV. use (hinhuniv _ HU); intros HA. use (hinhfun _ HV); intros HB. induction HA as [A HA]. induction HB as [B HB]. exists (λ x, ∃ a b, A a × B b × x = (a * b)%ring). intro p. assert (H0 : U p ∧ V p ⇔ A ⊈ p ∧ B ⊈ p). { use make_dirprod; intro H. - use make_dirprod. + apply (dirprod_pr1 (HA p)), (dirprod_pr1 H). + apply (dirprod_pr1 (HB p)), (dirprod_pr2 H). - use make_dirprod. + apply (dirprod_pr2 (HA p)), (dirprod_pr1 H). + apply (dirprod_pr2 (HB p)), (dirprod_pr2 H). } apply (logeq_trans H0). unfold subtype_notContainedIn. use make_dirprod; intro H. - use (hinhuniv _ (dirprod_pr1 H)); intro Ha. use (hinhfun _ (dirprod_pr2 H)); intro Hb. induction Ha as [a Ha]. induction Hb as [b Hb]. exists (a * b)%ring. use make_dirprod. + apply hinhpr. exists a, b. exact (make_dirprod (dirprod_pr1 Ha) (make_dirprod (dirprod_pr1 Hb) (idpath _))). + apply (@negf _ (p a ∨ p b)). * exact (prime_ideal_ax1 _ a b). * apply toneghdisj. exact (make_dirprod (dirprod_pr2 Ha) (dirprod_pr2 Hb)). - use (hinhuniv _ H); intro Hx. induction Hx as [x Hx]. induction Hx as [Hx Hpx]. use (hinhuniv _ Hx); intro Hab. induction Hab as [a Hab]. induction Hab as [b Hab]. induction Hab as [Ha Hab]. induction Hab as [Hb Hab]. use make_dirprod; apply hinhpr. + exists a. use make_dirprod. * exact Ha. * use (negf _ Hpx). intro Hpa. apply (transportb (λ y, p y) Hab). apply (ideal_isr p b a), Hpa. + exists b. use make_dirprod. * exact Hb. * use (negf _ Hpx). intro Hpb. apply (transportb (λ y, p y) Hab). apply (ideal_isl p a b), Hpb. Defined.
imports: UniMath.Algebra.RigsAndRings UniMath.Algebra.RigsAndRings.Ideals UniMath.MoreFoundations.AxiomOfChoice UniMath.MoreFoundations.Subtypes UniMath.Topology.Topology UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.Categories.Commring UniMath.AlgebraicGeometry.Topology UniMath.AlgebraicGeometry.SheavesOfRings