Commit 2023-05-21 19:38 92b28a1c

View on Github →

feat: port AlgebraicGeometry.ProjectiveSpectrum.Topology (#4171)

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Topology.lean

added theorem ProjectiveSpectrum.as_ideal_le_as_ideal

added theorem ProjectiveSpectrum.as_ideal_lt_as_ideal

added def ProjectiveSpectrum.basicOpen

added theorem ProjectiveSpectrum.basicOpen_eq_union_of_projection

added theorem ProjectiveSpectrum.basicOpen_eq_zeroLocus_compl

added theorem ProjectiveSpectrum.basicOpen_mul

added theorem ProjectiveSpectrum.basicOpen_mul_le_left

added theorem ProjectiveSpectrum.basicOpen_mul_le_right

added theorem ProjectiveSpectrum.basicOpen_one

added theorem ProjectiveSpectrum.basicOpen_pow

added theorem ProjectiveSpectrum.basicOpen_zero

added theorem ProjectiveSpectrum.coe_vanishingIdeal

added theorem ProjectiveSpectrum.gc_homogeneousIdeal

added theorem ProjectiveSpectrum.gc_ideal

added theorem ProjectiveSpectrum.gc_set

added theorem ProjectiveSpectrum.homogeneousIdeal_le_vanishingIdeal_zeroLocus

added theorem ProjectiveSpectrum.ideal_le_vanishingIdeal_zeroLocus

added theorem ProjectiveSpectrum.isClosed_iff_zeroLocus

added theorem ProjectiveSpectrum.isClosed_zeroLocus

added theorem ProjectiveSpectrum.isOpen_basicOpen

added theorem ProjectiveSpectrum.isOpen_iff

added theorem ProjectiveSpectrum.isTopologicalBasis_basic_opens

added theorem ProjectiveSpectrum.le_iff_mem_closure

added theorem ProjectiveSpectrum.mem_basicOpen

added theorem ProjectiveSpectrum.mem_coe_basicOpen

added theorem ProjectiveSpectrum.mem_compl_zeroLocus_iff_not_mem

added theorem ProjectiveSpectrum.mem_vanishingIdeal

added theorem ProjectiveSpectrum.mem_zeroLocus

added theorem ProjectiveSpectrum.subset_vanishingIdeal_zeroLocus

added theorem ProjectiveSpectrum.subset_zeroLocus_iff_le_vanishingIdeal

added theorem ProjectiveSpectrum.subset_zeroLocus_iff_subset_vanishingIdeal

added theorem ProjectiveSpectrum.subset_zeroLocus_vanishingIdeal

added theorem ProjectiveSpectrum.sup_vanishingIdeal_le

added def ProjectiveSpectrum.top

added theorem ProjectiveSpectrum.union_zeroLocus

added def ProjectiveSpectrum.vanishingIdeal

added theorem ProjectiveSpectrum.vanishingIdeal_anti_mono

added theorem ProjectiveSpectrum.vanishingIdeal_closure

added theorem ProjectiveSpectrum.vanishingIdeal_iUnion

added theorem ProjectiveSpectrum.vanishingIdeal_singleton

added theorem ProjectiveSpectrum.vanishingIdeal_union

added theorem ProjectiveSpectrum.vanishingIdeal_univ

added def ProjectiveSpectrum.zeroLocus

added theorem ProjectiveSpectrum.zeroLocus_anti_mono

added theorem ProjectiveSpectrum.zeroLocus_anti_mono_homogeneousIdeal

added theorem ProjectiveSpectrum.zeroLocus_anti_mono_ideal

added theorem ProjectiveSpectrum.zeroLocus_bUnion

added theorem ProjectiveSpectrum.zeroLocus_bot

added theorem ProjectiveSpectrum.zeroLocus_empty

added theorem ProjectiveSpectrum.zeroLocus_empty_of_one_mem

added theorem ProjectiveSpectrum.zeroLocus_iSup_homogeneousIdeal

added theorem ProjectiveSpectrum.zeroLocus_iSup_ideal

added theorem ProjectiveSpectrum.zeroLocus_iUnion

added theorem ProjectiveSpectrum.zeroLocus_inf

added theorem ProjectiveSpectrum.zeroLocus_mul_homogeneousIdeal

added theorem ProjectiveSpectrum.zeroLocus_mul_ideal

added theorem ProjectiveSpectrum.zeroLocus_singleton_mul

added theorem ProjectiveSpectrum.zeroLocus_singleton_one

added theorem ProjectiveSpectrum.zeroLocus_singleton_pow

added theorem ProjectiveSpectrum.zeroLocus_singleton_zero

added theorem ProjectiveSpectrum.zeroLocus_span

added theorem ProjectiveSpectrum.zeroLocus_sup_homogeneousIdeal

added theorem ProjectiveSpectrum.zeroLocus_sup_ideal

added theorem ProjectiveSpectrum.zeroLocus_union

added theorem ProjectiveSpectrum.zeroLocus_univ

added theorem ProjectiveSpectrum.zeroLocus_vanishingIdeal_eq_closure

added structure ProjectiveSpectrum