Commit 2024-07-26 10:22 75defd20

View on Github →

feat(RingTheory): Surjective on stalks ring homomorphisms. (#14377)

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicGeometry/PrimeSpectrum/TensorProduct.lean

added theorem PrimeSpectrum.continuous_tensorProductTo

added theorem PrimeSpectrum.embedding_tensorProductTo_of_surjectiveOnStalks

added theorem PrimeSpectrum.embedding_tensorProductTo_of_surjectiveOnStalks_aux

added def PrimeSpectrum.tensorProductTo

Created Mathlib/RingTheory/SurjectiveOnStalks.lean

added theorem RingHom.SurjectiveOnStalks.baseChange

added theorem RingHom.SurjectiveOnStalks.comp

added theorem RingHom.SurjectiveOnStalks.exists_mul_eq_tmul

added theorem RingHom.SurjectiveOnStalks.of_comp

added def RingHom.SurjectiveOnStalks

added theorem RingHom.surjectiveOnStalks_iff_forall_ideal

added theorem RingHom.surjectiveOnStalks_iff_forall_maximal'

added theorem RingHom.surjectiveOnStalks_iff_forall_maximal

added theorem RingHom.surjectiveOnStalks_iff_of_isLocalRingHom

added theorem RingHom.surjectiveOnStalks_of_exists_div

added theorem RingHom.surjectiveOnStalks_of_isLocalization

added theorem RingHom.surjectiveOnStalks_of_surjective

added theorem RingHom.surjective_localRingHom_iff

Modified Mathlib/Topology/Sets/Opens.lean

added theorem TopologicalSpace.Opens.IsBasis.le_iff