Commit 2023-05-24 09:36 5719f012

View on Github →

feat: port AlgebraicGeometry.PrimeSpectrum.Basic (#4276)

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean

added theorem LocalRing.PrimeSpectrum.comap_residue

added def LocalRing.closedPoint

added theorem LocalRing.closedPoint_mem_iff

added theorem LocalRing.comap_closedPoint

added theorem LocalRing.isLocalRingHom_iff_comap_closedPoint

added theorem LocalRing.specializes_closedPoint

added theorem PrimeSpectrum.asIdeal_le_asIdeal

added theorem PrimeSpectrum.asIdeal_lt_asIdeal

added def PrimeSpectrum.basicOpen

added theorem PrimeSpectrum.basicOpen_eq_bot_iff

added theorem PrimeSpectrum.basicOpen_eq_zeroLocus_compl

added theorem PrimeSpectrum.basicOpen_le_basicOpen_iff

added theorem PrimeSpectrum.basicOpen_mul

added theorem PrimeSpectrum.basicOpen_mul_le_left

added theorem PrimeSpectrum.basicOpen_mul_le_right

added theorem PrimeSpectrum.basicOpen_one

added theorem PrimeSpectrum.basicOpen_pow

added theorem PrimeSpectrum.basicOpen_zero

added theorem PrimeSpectrum.closedEmbedding_comap_of_surjective

added def PrimeSpectrum.closedsEmbedding

added theorem PrimeSpectrum.closure_singleton

added theorem PrimeSpectrum.coe_vanishingIdeal

added def PrimeSpectrum.comap

added theorem PrimeSpectrum.comap_asIdeal

added theorem PrimeSpectrum.comap_comp

added theorem PrimeSpectrum.comap_comp_apply

added theorem PrimeSpectrum.comap_id

added theorem PrimeSpectrum.comap_inducing_of_surjective

added theorem PrimeSpectrum.comap_injective_of_surjective

added theorem PrimeSpectrum.comap_singleton_isClosed_of_isIntegral

added theorem PrimeSpectrum.comap_singleton_isClosed_of_surjective

added theorem PrimeSpectrum.gc

added theorem PrimeSpectrum.gc_set

added theorem PrimeSpectrum.image_comap_zeroLocus_eq_zeroLocus_comap

added theorem PrimeSpectrum.isBasis_basic_opens

added theorem PrimeSpectrum.isClosed_iff_zeroLocus

added theorem PrimeSpectrum.isClosed_iff_zeroLocus_ideal

added theorem PrimeSpectrum.isClosed_iff_zeroLocus_radical_ideal

added theorem PrimeSpectrum.isClosed_range_comap_of_surjective

added theorem PrimeSpectrum.isClosed_singleton_iff_isMaximal

added theorem PrimeSpectrum.isClosed_zeroLocus

added theorem PrimeSpectrum.isCompact_basicOpen

added theorem PrimeSpectrum.isIrreducible_iff_vanishingIdeal_isPrime

added theorem PrimeSpectrum.isIrreducible_zeroLocus_iff

added theorem PrimeSpectrum.isIrreducible_zeroLocus_iff_of_radical

added theorem PrimeSpectrum.isOpen_basicOpen

added theorem PrimeSpectrum.isOpen_iff

added theorem PrimeSpectrum.isRadical_vanishingIdeal

added theorem PrimeSpectrum.isTopologicalBasis_basic_opens

added theorem PrimeSpectrum.le_iff_mem_closure

added theorem PrimeSpectrum.le_iff_specializes

added theorem PrimeSpectrum.le_vanishingIdeal_zeroLocus

added def PrimeSpectrum.localizationMapOfSpecializes

added theorem PrimeSpectrum.localization_away_comap_range

added theorem PrimeSpectrum.localization_away_openEmbedding

added theorem PrimeSpectrum.localization_comap_embedding

added theorem PrimeSpectrum.localization_comap_inducing

added theorem PrimeSpectrum.localization_comap_injective

added theorem PrimeSpectrum.localization_comap_range

added theorem PrimeSpectrum.mem_basicOpen

added theorem PrimeSpectrum.mem_compl_zeroLocus_iff_not_mem

added theorem PrimeSpectrum.mem_vanishingIdeal

added theorem PrimeSpectrum.mem_zeroLocus

added def PrimeSpectrum.nhdsOrderEmbedding

added theorem PrimeSpectrum.pUnit

added theorem PrimeSpectrum.preimage_comap_zeroLocus

added theorem PrimeSpectrum.preimage_comap_zeroLocus_aux

added def PrimeSpectrum.primeSpectrumProdOfSum

added theorem PrimeSpectrum.primeSpectrumProd_symm_inl_asIdeal

added theorem PrimeSpectrum.primeSpectrumProd_symm_inr_asIdeal

added theorem PrimeSpectrum.range_comap_of_surjective

added theorem PrimeSpectrum.subset_vanishingIdeal_zeroLocus

added theorem PrimeSpectrum.subset_zeroLocus_iff_le_vanishingIdeal

added theorem PrimeSpectrum.subset_zeroLocus_iff_subset_vanishingIdeal

added theorem PrimeSpectrum.subset_zeroLocus_vanishingIdeal

added theorem PrimeSpectrum.sup_vanishingIdeal_le

added theorem PrimeSpectrum.t1Space_iff_isField

added theorem PrimeSpectrum.union_zeroLocus

added def PrimeSpectrum.vanishingIdeal

added theorem PrimeSpectrum.vanishingIdeal_anti_mono

added theorem PrimeSpectrum.vanishingIdeal_anti_mono_iff

added theorem PrimeSpectrum.vanishingIdeal_closure

added theorem PrimeSpectrum.vanishingIdeal_eq_top_iff

added theorem PrimeSpectrum.vanishingIdeal_iUnion

added theorem PrimeSpectrum.vanishingIdeal_singleton

added theorem PrimeSpectrum.vanishingIdeal_strict_anti_mono_iff

added theorem PrimeSpectrum.vanishingIdeal_union

added theorem PrimeSpectrum.vanishingIdeal_univ

added theorem PrimeSpectrum.vanishingIdeal_zeroLocus_eq_radical

added def PrimeSpectrum.zeroLocus

added theorem PrimeSpectrum.zeroLocus_anti_mono

added theorem PrimeSpectrum.zeroLocus_anti_mono_ideal

added theorem PrimeSpectrum.zeroLocus_bUnion

added theorem PrimeSpectrum.zeroLocus_bot

added theorem PrimeSpectrum.zeroLocus_empty

added theorem PrimeSpectrum.zeroLocus_empty_iff_eq_top

added theorem PrimeSpectrum.zeroLocus_empty_of_one_mem

added theorem PrimeSpectrum.zeroLocus_iSup

added theorem PrimeSpectrum.zeroLocus_iUnion

added theorem PrimeSpectrum.zeroLocus_inf

added theorem PrimeSpectrum.zeroLocus_mul

added theorem PrimeSpectrum.zeroLocus_pow

added theorem PrimeSpectrum.zeroLocus_radical

added theorem PrimeSpectrum.zeroLocus_singleton_mul

added theorem PrimeSpectrum.zeroLocus_singleton_one

added theorem PrimeSpectrum.zeroLocus_singleton_pow

added theorem PrimeSpectrum.zeroLocus_singleton_zero

added theorem PrimeSpectrum.zeroLocus_span

added theorem PrimeSpectrum.zeroLocus_subset_zeroLocus_iff

added theorem PrimeSpectrum.zeroLocus_subset_zeroLocus_singleton_iff

added theorem PrimeSpectrum.zeroLocus_sup

added theorem PrimeSpectrum.zeroLocus_union

added theorem PrimeSpectrum.zeroLocus_univ

added theorem PrimeSpectrum.zeroLocus_vanishingIdeal_eq_closure

added structure PrimeSpectrum