Commit 2025-04-10 13:59 18138f8a

View on Github →

feat(RingTheory/Spectrum/Prime): purely inseparable extensions induce universal homeomorphisms (#23491) Co-authored by: Junyan Xu

Estimated changes

Modified Mathlib.lean

Modified Mathlib/FieldTheory/PurelyInseparable/Basic.lean

added theorem IsPurelyInseparable.exists_pow_mem_range_tensorProduct

added theorem IsPurelyInseparable.exists_pow_pow_mem_range_tensorProduct_of_expChar

added theorem Subalgebra.mem_perfectClosure_iff

added def Subalgebra.perfectClosure

Modified Mathlib/FieldTheory/PurelyInseparable/PerfectClosure.lean

Modified Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean

deleted theorem TensorProduct.mk_surjective

Modified Mathlib/RingTheory/Spectrum/Prime/Basic.lean

added theorem PrimeSpectrum.zeroLocus_nilradical

Created Mathlib/RingTheory/Spectrum/Prime/Homeomorph.lean

added theorem PrimeSpectrum.isHomeomorph_comap

added theorem PrimeSpectrum.isHomeomorph_comap_of_isPurelyInseparable

added theorem PrimeSpectrum.isHomeomorph_comap_tensorProductMap_of_isPurelyInseparable

Modified Mathlib/RingTheory/Spectrum/Prime/Topology.lean

added theorem PrimeSpectrum.comap_quotientMk_bijective_of_le_nilradical

added def PrimeSpectrum.homeomorphOfRingEquiv

added theorem PrimeSpectrum.isHomeomorph_comap_of_bijective

added theorem RingHom.IsIntegral.specComap_surjective

Modified Mathlib/RingTheory/TensorProduct/Basic.lean

added theorem Algebra.TensorProduct.cancelBaseChange_symm_tmul

added theorem Algebra.TensorProduct.cancelBaseChange_tmul

added theorem Algebra.TensorProduct.includeLeft_surjective

added theorem Algebra.TensorProduct.includeRight_surjective

added theorem Algebra.TensorProduct.tmul_one_eq_one_tmul

added theorem LinearMap.map_mul_of_map_mul_tmul

added theorem TensorProduct.flip_mk_surjective

added theorem TensorProduct.mk_surjective