galRestrict'_galLift — Mathlib

English

Restricting a map via galRestrict equals applying galRestrictHom.

Русский

Ограничение отображения через galRestrict равно применению galRestrictHom.

LaTeX

$$galRestrict_apply (σ : L ≃ₐ[K] L) (x : B) : galRestrict A K L B σ x = galRestrictHom A K L B σ x$$

Lean4

@[simp]
theorem galRestrict'_galLift (σ : B →ₐ[A] B₂) : galRestrict' A B B₂ (galLift K L L₂ σ) = σ :=
  have := (IsFractionRing.injective A K).isDomain
  have := IsIntegralClosure.isLocalization A K L B
  AlgHom.ext fun x ↦
    IsIntegralClosure.algebraMap_injective B₂ A L₂ (by simp [galRestrict', Subalgebra.algebraMap_eq, galLift])

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