isScalarTower_over_bot — Mathlib

English

The scalar action of F on E factors through the bottom intermediate field, giving a consistent IsScalarTower structure.

Русский

Действие скаляров F на E факторизуется через нижнее промежуточное поле, образуя согласованную структуру IsScalarTower.

LaTeX

$$$ IsScalarTower (\\bot : \\text{IntermediateField}(F,E)) F E $$$

Lean4

instance isScalarTower_over_bot : IsScalarTower (⊥ : IntermediateField F E) F E :=
  IsScalarTower.of_algebraMap_eq
    (by
      intro x
      obtain ⟨y, rfl⟩ := (botEquiv F E).symm.surjective x
      rw [coe_algebraMap_over_bot, (botEquiv F E).apply_symm_apply, botEquiv_symm,
        IsScalarTower.algebraMap_apply F (⊥ : IntermediateField F E) E])

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