toUnder — Mathlib

English

Definition that converts an algebra map into a morphism in Under R.

Русский

Определение преобразования алгебраического отображения в морфизм в Under R.

LaTeX

$$$\text{toUnder}(f) : \text{Under}(R) \to \text{Under}(R)$-м morphism$$

Lean4

/-- Make an isomorphism in `Under R` from an algebra isomorphism. -/
def toUnder {A B : Type u} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (f : A ≃ₐ[R] B) :
    CommRingCat.mkUnder R A ≅ CommRingCat.mkUnder R B
    where
  hom := f.toAlgHom.toUnder
  inv := f.symm.toAlgHom.toUnder
  hom_inv_id := by
    ext (a : (CommRingCat.mkUnder R A).right)
    simp
  inv_hom_id := by
    ext a
    simp

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