English
For σ: B →ₐ[A] B and σ': B₂ →ₐ[A] B₃, the lift respects composition: galLift(σ' ∘ σ) = (galLift σ') ∘ (galLift σ).
Русский
Подъем сохраняет композицию: galLift(σ' ∘ σ) = galLift(σ') ∘ galLift(σ).
LaTeX
$$galLift_comp (σ : B →ₐ[A] B) (σ' : B₂ →ₐ[A] B₃) : galLift K L L₃ (σ'.comp σ) = (galLift K L₂ L₃ σ').comp (galLift K L L₂ σ)$$
Lean4
theorem galLift_comp [Algebra.IsAlgebraic K L₂] (σ : B →ₐ[A] B₂) (σ' : B₂ →ₐ[A] B₃) :
galLift K L L₃ (σ'.comp σ) = (galLift K L₂ L₃ σ').comp (galLift K L L₂ σ) :=
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
