baseChange_dblU — Mathlib

English

Base change commutes with dblU: (W'.baseChange K).toProjective.dblU (f ∘ P) = f ((W'.baseChange F).toProjective.dblU P).

Русский

Базовое изменение сохраняет dblU: (W'.baseChange K).toProjective.dblU (f ∘ P) = f ((W'.baseChange F).toProjective.dblU P).

LaTeX

$$ (W'.baseChange K).toProjective.dblU (f \circ P) = f ((W'.baseChange F).toProjective.dblU P) $$

Lean4

theorem baseChange_dblU [Algebra R F] [Algebra S F] [IsScalarTower R S F] [Algebra R K] [Algebra S K]
    [IsScalarTower R S K] (f : F →ₐ[S] K) (P : Fin 3 → F) :
    (W'.baseChange K).toProjective.dblU (f ∘ P) = f ((W'.baseChange F).toProjective.dblU P) := by
  rw [← RingHom.coe_coe, ← map_dblU, map_baseChange]

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