base_change — Mathlib

English

If R ⟶ A is a FormallyUnramified extension and B is any R-algebra, then B ⊗_R A is FormallyUnramified over B.

Русский

Если R ⟶ A — формально неразветвленное расширение, и B — любая R-алгебра, то B ⊗_R A неразветвлено над B.

LaTeX

$$$[\text{FormallyUnramified } R \; A] \Rightarrow [\text{FormallyUnramified } B \; (B \otimes_R A)]$$$

Lean4

instance base_change [FormallyUnramified R A] : FormallyUnramified B (B ⊗[R] A) :=
  by
  rw [iff_comp_injective]
  intro C _ _ I hI f₁ f₂ e
  letI := ((algebraMap B C).comp (algebraMap R B)).toAlgebra
  haveI : IsScalarTower R B C := IsScalarTower.of_algebraMap_eq' rfl
  ext : 1
  · subsingleton
  · exact FormallyUnramified.ext I ⟨2, hI⟩ fun x => AlgHom.congr_fun e (1 ⊗ₜ x)

Похожие утверждения