Chevalley

📁 Source: Mathlib/RingTheory/Spectrum/Prime/Chevalley.lean

Statistics

Metric	Count
Definitions	0
Theorems isConstructible_comap_C, isConstructible_comap_image, isConstructible_range_comap, isOpenMap_comap_algebraMap_tensorProduct_of_field, isOpenMap_comap_of_hasGoingDown_of_finitePresentation	5
Total	5

PrimeSpectrum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isConstructible_comap_C 📖	mathematical	Topology.IsConstructible PrimeSpectrum Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.commSemiring zariskiTopology	Set.image comap Polynomial.C	—	exists_constructibleSetData_iff IsScalarTower.right ChevalleyThm.chevalley_polynomialC Submodule.mem_top ConstructibleSetData.isConstructible_toSet
isConstructible_comap_image 📖	mathematical	Topology.IsConstructible PrimeSpectrum CommRing.toCommSemiring zariskiTopology	Set.image comap	—	RingHom.FinitePresentation.polynomial_induction isConstructible_comap_C RingHom.instRingHomClass Topology.IsConstructible.image_of_isClosedEmbedding isClosedEmbedding_comap_of_surjective range_comap_of_surjective isRetrocompact_zeroLocus_compl_of_fg Set.image_congr Set.image_comp
isConstructible_range_comap 📖	mathematical	—	Topology.IsConstructible PrimeSpectrum CommRing.toCommSemiring zariskiTopology Set.range comap	—	isConstructible_comap_image Topology.IsConstructible.univ Set.image_univ
isOpenMap_comap_algebraMap_tensorProduct_of_field 📖	mathematical	—	IsOpenMap PrimeSpectrum TensorProduct Semifield.toCommSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule CommSemiring.toSemiring CommRing.toCommSemiring Algebra.TensorProduct.instCommSemiring zariskiTopology comap algebraMap Algebra.TensorProduct.instSemiring Algebra.TensorProduct.leftAlgebra Algebra.id Algebra.to_smulCommClass	—	Algebra.to_smulCommClass exists_fg_and_mem_baseChange Algebra.FinitePresentation.of_finiteType IsSimpleModule.instIsNoetherian instIsSimpleModule Subalgebra.fg_top Set.ext isPrime mem_image_comap_basicOpen not_iff_not IsScalarTower.to_smulCommClass IsScalarTower.right TensorProduct.isScalarTower_left IsLocalRing.instIsScalarTowerResidueField OreLocalization.instIsScalarTower Algebra.TensorProduct.ext TensorProduct.isScalarTower TensorProduct.smulCommClass_left IsScalarTower.to_smulCommClass' Algebra.ext_id AlgHom.ext AlgHom.restrictScalars.congr_simp Algebra.TensorProduct.map_comp_includeLeft Algebra.TensorProduct.cancelBaseChange_tmul one_smul Algebra.TensorProduct.cancelBaseChange_symm_tmul Ideal.ResidueField.algHom_ext EquivLike.toEmbeddingLike Module.Flat.lTensor_preserves_injective_linearMap Module.FaithfullyFlat.toFlat Module.FaithfullyFlat.instOfNontrivialOfFree IsLocalRing.toNontrivial Field.instIsLocalRing Module.Free.of_divisionRing Subtype.val_injective IsNilpotent.map_iff RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass isOpenMap_comap_of_hasGoingDown_of_finitePresentation Algebra.HasGoingDown.of_flat Module.Flat.baseChange Module.Flat.of_free Algebra.FinitePresentation.baseChange TopologicalSpace.Opens.isOpen eq_biUnion_of_isOpen Set.image_iUnion₂ isOpen_iUnion
isOpenMap_comap_of_hasGoingDown_of_finitePresentation 📖	mathematical	—	IsOpenMap PrimeSpectrum CommRing.toCommSemiring zariskiTopology comap algebraMap CommSemiring.toSemiring	—	TopologicalSpace.IsTopologicalBasis.isOpenMap_iff isBasis_basic_opens isOpen_of_stableUnderGeneralization_of_isConstructible StableUnderGeneralization.image Algebra.HasGoingDown.iff_generalizingMap_primeSpectrumComap IsOpen.stableUnderGeneralization TopologicalSpace.Opens.is_open' isConstructible_comap_image RingHom.finitePresentation_algebraMap isConstructible_basicOpen

---

← Back to Index