galLift_galRestrict' — Mathlib

English

The restriction after lifting returns the original map: galRestrict'(galLift(σ)) = σ.

Русский

Ограничение после подъема возвращает исходное отображение: galRestrict'(galLift(σ)) = σ.

LaTeX

$$galRestrict'_galLift (σ : B →ₐ[A] B₂) : galRestrict' A B B₂ (galLift K L L₂ σ) = σ$$

Lean4

@[simp]
theorem galLift_galRestrict' (σ : L →ₐ[K] L₂) : galLift K L L₂ (galRestrict' A B B₂ σ) = σ :=
  have := (IsFractionRing.injective A K).isDomain
  have := IsIntegralClosure.isLocalization A K L B
  AlgHom.coe_ringHom_injective <|
    IsLocalization.ringHom_ext (Algebra.algebraMapSubmonoid B A⁰) <|
      RingHom.ext fun x ↦ by simp [galRestrict', Subalgebra.algebraMap_eq, galLift]

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