fieldEquivOfAlgEquiv — Mathlib

English

If the range of g equals the closure of s, then the fieldRange of lift hg equals the closure of s.

Русский

Если range g равно замыканию s, тогда fieldRange lift hg равно замыканию s.

LaTeX

$$$ (\mathrm{lift} \; hg).fieldRange = \operatorname{Subfield.closure} s $$$

Lean4

/-- An algebra isomorphism of rings induces an algebra isomorphism of fraction fields. -/
noncomputable def fieldEquivOfAlgEquiv (f : B ≃ₐ[A] C) : FB ≃ₐ[FA] FC
    where
  __ := IsFractionRing.ringEquivOfRingEquiv f.toRingEquiv
  commutes'
    x := by
    obtain ⟨x, y, -, rfl⟩ := IsFractionRing.div_surjective (A := A) x
    simp_rw [map_div₀, ← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply A B FB]
    simp [← IsScalarTower.algebraMap_apply A C FC]

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