English
Purely inseparable field extensions induce universal homeomorphisms on Spec via comap maps.
Русский
Чисто неразложимые расширения полей индуцируют универсальные гомоморфизмы спектра.
LaTeX
$$$IsHomeomorph\\ (\\operatorname{comap}\\; (\\mathrm{algebraMap}\\; R \\; (R \\otimes_k K)))$$$
Lean4
/-- If `L` is a purely inseparable extension of `K` over `R` and `S` is an `R`-algebra,
the induced map `Spec (L ⊗[R] S) ⟶ Spec (K ⊗[R] S)` is a homeomorphism. -/
theorem isHomeomorph_comap_tensorProductMap_of_isPurelyInseparable [Algebra R K] [Algebra R S] (L : Type*) [Field L]
[Algebra R L] [Algebra K L] [IsScalarTower R K L] [IsPurelyInseparable K L] :
IsHomeomorph (comap (Algebra.TensorProduct.map (Algebra.ofId K L) (.id R S)).toRingHom) :=
by
let e : (L ⊗[R] S) ≃ₐ[K] L ⊗[K] (K ⊗[R] S) := (Algebra.TensorProduct.cancelBaseChange R K K L S).symm
let e2 : L ⊗[K] (K ⊗[R] S) ≃ₐ[K] (K ⊗[R] S) ⊗[K] L := Algebra.TensorProduct.comm ..
have heq :
Algebra.TensorProduct.map (Algebra.ofId K L) (AlgHom.id R S) =
(e.symm.toAlgHom.comp e2.symm.toAlgHom).comp (IsScalarTower.toAlgHom K (K ⊗[R] S) ((K ⊗[R] S) ⊗[K] L)) :=
by ext; simp [e, e2]
rw [heq]
simp only [AlgEquiv.toAlgHom_eq_coe, AlgHom.toRingHom_eq_coe, AlgHom.comp_toRingHom, AlgEquiv.toAlgHom_toRingHom,
IsScalarTower.coe_toAlgHom, comap_comp, ContinuousMap.coe_comp]
exact
(isHomeomorph_comap_of_isPurelyInseparable K L (K ⊗[R] S)).comp <|
(isHomeomorph_comap_of_bijective e2.symm.bijective).comp <| isHomeomorph_comap_of_bijective e.symm.bijective
