map — Mathlib

English

For f: L →ₐ[K] L' and S an intermediate field of L, S.map f is the intermediate field between K and L' consisting of all x ∈ L' with a preimage in S under f.

Русский

Для отображения f: L →ₐ[K] L' и S — промежуточного поля L, S.map f — промежуточное поле между K и L', состоящее из всех x ∈ L' с предобразом в S по f.

LaTeX

$$$ x \\in S.map f \\iff \\exists y\\in S, f(y) = x $$$

Lean4

/-- Given `f : L →ₐ[K] L'`, `S.map f` is the intermediate field between `K` and `L'`
such that `x ∈ S ↔ f x ∈ S.map f`. -/
def map (f : L →ₐ[K] L') (S : IntermediateField K L) : IntermediateField K L'
    where
  __ := S.toSubalgebra.map f
  inv_mem' := by
    rintro _ ⟨x, hx, rfl⟩
    exact ⟨x⁻¹, S.inv_mem hx, map_inv₀ f x⟩

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