English
Given an algebra hom f: L →ₐ[K] L' and an intermediate field S ⊆ L', the comap S f is the intermediate field of K ⊆ L consisting of elements mapped into S by f, with the inverse-memory property f(x) ∈ S ↔ x ∈ S.comap f.
Русский
Дано алгебраическое отображение f: L →ₐ[K] L' и промежуточное поле S ⊆ L'. Комап S f — это промежуточное поле между K и L, состоящее из элементов, которые маппятся в S под f; свойство f(x) ∈ S ↔ x ∈ S.comap f.
LaTeX
$$$\\forall x\\in L:\\ f(x)\\in S \\iff x\\in S^{\\mathrm{comap}(f)}$$$
Lean4
/-- Given `f : L →ₐ[K] L'`, `S.comap f` is the intermediate field between `K` and `L`
such that `f x ∈ S ↔ x ∈ S.comap f`. -/
def comap (f : L →ₐ[K] L') (S : IntermediateField K L') : IntermediateField K L
where
__ := S.toSubalgebra.comap f
inv_mem' x hx := show f x⁻¹ ∈ S by rw [map_inv₀ f x]; exact S.inv_mem hx
