galLiftEquiv_algebraMap_apply — Mathlib

English

Equality expressing galRestrict' in terms of the integral closure equivalence with the codRestrict construction.

Русский

Равенство, выражающее galRestrict' через эквивалентность интегрального замыкания и конструкцию codRestrict.

LaTeX

$$galRestrict'_eq_1 (A) {L₂} {L} (B) (B₂) [IsIntegralClosure B A L] (f : L →ₐ[K] L₂) : Eq (galRestrict' A B B (f)) ((IsIntegralClosure.equiv A (Subtype fun x => SetLike.instMembership.mem (integralClosure A L₂) x) L₂ B₂).toAlgHom • (…))$$

Lean4

theorem galLiftEquiv_algebraMap_apply [Algebra.IsAlgebraic K L₂] (σ : B ≃ₐ[A] B₂) (x : B) :
    galLiftEquiv K L L₂ σ (algebraMap B L x) = algebraMap B₂ L₂ (σ x) := by simp [galLiftEquiv]

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