English
Applying the restrictNormalHom map to a normal extension, evaluated on a specified f, yields the same as restricting first and then applying.
Русский
Применение restrictNormalHom к нормальному расширению к элементу f даёт тот же результат, что ограничение сначала, затем применение.
LaTeX
$$$\text{restrictNormalHom}(f) = \text{RestrictNormalHom}(f)$$$
Lean4
/-- The normalized trace map from an algebraic extension `K` to the base field `F`. -/
noncomputable def normalizedTrace : K →ₗ[F] F
where
toFun := normalizedTraceAux F K
map_add' a
b := by
let E := F⟮a⟯ ⊔ F⟮b⟯
have : FiniteDimensional F F⟮a⟯ := adjoin.finiteDimensional (IsIntegral.isIntegral a)
have : FiniteDimensional F F⟮b⟯ := adjoin.finiteDimensional (IsIntegral.isIntegral b)
have ha : a ∈ E := (le_sup_left : F⟮a⟯ ≤ E) <| mem_adjoin_simple_self F a
have hb : b ∈ E := (le_sup_right : F⟮b⟯ ≤ E) <| mem_adjoin_simple_self F b
have hab : a + b ∈ E := IntermediateField.add_mem E ha hb
let a' : E := ⟨a, ha⟩
let b' : E := ⟨b, hb⟩
let ab' : E := ⟨a + b, hab⟩
rw [normalizedTraceAux_intermediateField F K a', normalizedTraceAux_intermediateField F K b',
normalizedTraceAux_intermediateField F K ab', normalizedTraceAux_eq_of_fininteDimensional F a',
normalizedTraceAux_eq_of_fininteDimensional F b', normalizedTraceAux_eq_of_fininteDimensional F ab', ← smul_add, ←
map_add, AddMemClass.mk_add_mk]
map_smul' m
a := by
dsimp only [AddHom.toFun_eq_coe, AddHom.coe_mk, RingHom.id_apply]
let E := F⟮a⟯
have : FiniteDimensional F F⟮a⟯ := adjoin.finiteDimensional (IsIntegral.isIntegral a)
have ha : a ∈ E := mem_adjoin_simple_self F a
have hma : m • a ∈ E := smul_mem E ha
let a' : E := ⟨a, ha⟩
let ma' : E := ⟨m • a, hma⟩
rw [normalizedTraceAux_intermediateField F K a', normalizedTraceAux_intermediateField F K ma',
normalizedTraceAux_eq_of_fininteDimensional F a', normalizedTraceAux_eq_of_fininteDimensional F ma', smul_comm, ←
map_smul _ m, SetLike.mk_smul_mk]
