English
Transfers IsAdjoinRoot across an algebra isomorphism: given e: S ≃ₐ[R] T, h.ofAlgEquiv e is IsAdjoinRoot T f with map := e.map ∘ h.map.
Русский
Переносит IsAdjoinRoot через алгебраическое изоморфизм: данный e определяет IsAdjoinRoot T f через композицию.
LaTeX
$$ofAlgEquiv : IsAdjoinRoot T f$$
Lean4
/-- Transfer `IsAdjoinRoot` across an algebra isomorphism.
This is the converse of `IsAdjoinRoot.algEquiv`: this turns an `AlgEquiv` into an `IsAdjoinRoot`,
and `IsAdjoinRoot.algEquiv` turns an `IsAdjoinRoot` into an `AlgEquiv`.
-/
@[simps! map_apply]
def ofAlgEquiv (e : S ≃ₐ[R] T) : IsAdjoinRoot T f
where
map := (e : S →ₐ[R] T).comp h.map
map_surjective := e.surjective.comp h.map_surjective
ker_map := by ext; simp [Ideal.mem_span_singleton]
