liftNormal — Mathlib

English

Restrict the lifted normal automorphism back to the original domain recovers the original automorphism.

Русский

Ограничение поднятого нормального автоморфизма приводит к исходному автоморфизму.

LaTeX

$$(\chi.liftNormal E).restrictNormal K₁ = χ$$

Lean4

/-- If `E/Kᵢ/F` are towers of fields with `E/F` normal then we can lift
  an algebra homomorphism `ϕ : K₁ →ₐ[F] K₂` to `ϕ.liftNormal E : E →ₐ[F] E`. -/
@[stacks 0BME "Part 2"]
noncomputable def liftNormal [h : Normal F E] : E →ₐ[F] E :=
  @AlgHom.restrictScalars F K₁ E E _ _ _ _ _ _ ((IsScalarTower.toAlgHom F K₂ E).comp ϕ).toRingHom.toAlgebra _ _ _ _ <|
    Nonempty.some <|
      @IntermediateField.nonempty_algHom_of_adjoin_splits _ _ _ _ _ _ _
        ((IsScalarTower.toAlgHom F K₂ E).comp ϕ).toRingHom.toAlgebra _
        (fun x _ ↦
          ⟨(h.out x).1.tower_top,
            splits_of_splits_of_dvd _ (map_ne_zero (minpoly.ne_zero (h.out x).1))
              (by
                rw [splits_map_iff, ← IsScalarTower.algebraMap_eq]
                exact (h.out x).2)
              (minpoly.dvd_map_of_isScalarTower F K₁ x)⟩)
        (IntermediateField.adjoin_univ _ _)

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