English
For a map of rings, the comap preimage of freeLocus is contained in the freeLocus after tensoring with the target ring.
Русский
Для отображения колец прообраз через comap свободного локуса вложен в свободный локус после тензорного произведения с кольцом-образом.
LaTeX
$$$\mathrm{comap}(\text{algebraMap } R \to A)^{-1}'\mathrm{freeLocus}(R,M) \le \mathrm{freeLocus}(A, A \otimes_R M)$$$
Lean4
theorem comap_freeLocus_le {A} [CommRing A] [Algebra R A] :
comap (algebraMap R A) ⁻¹' freeLocus R M ≤ freeLocus A (A ⊗[R] M) :=
by
intro p hp
let Rₚ := Localization.AtPrime (comap (algebraMap R A) p).asIdeal
let Aₚ := Localization.AtPrime p.asIdeal
rw [Set.mem_preimage, mem_freeLocus_iff_tensor _ Rₚ] at hp
rw [mem_freeLocus_iff_tensor _ Aₚ]
letI algebra : Algebra Rₚ Aₚ :=
(Localization.localRingHom (comap (algebraMap R A) p).asIdeal p.asIdeal (algebraMap R A) rfl).toAlgebra
have : IsScalarTower R Rₚ Aₚ :=
IsScalarTower.of_algebraMap_eq'
(by
simp [Rₚ, Aₚ, algebra, RingHom.algebraMap_toAlgebra, Localization.localRingHom, ← IsScalarTower.algebraMap_eq])
let e := AlgebraTensorModule.cancelBaseChange R Rₚ Aₚ Aₚ M ≪≫ₗ (AlgebraTensorModule.cancelBaseChange R A Aₚ Aₚ M).symm
exact .of_equiv e
