English
There is an equivalence between FGAlgCat R and a morphism-property under-category of finite-type maps from R.
Русский
Существует эквивалентность между FGAlgCat R и Under-категорией конечного типа морфизмов из R.
LaTeX
$$$FGAlgCat(R) \simeq Under( toMorphismProperty(FiniteType) \,, \top R)$$$
Lean4
/-- The category of finitely generated `R`-algebras is equivalent to the category of
finite type ring homomorphisms from `R`. -/
def equivUnder (R : CommRingCat.{u}) : FGAlgCat R ≌ MorphismProperty.Under (toMorphismProperty FiniteType) ⊤ R
where
functor.obj
A := ⟨(commAlgCatEquivUnder R).functor.obj A.obj, (RingHom.finiteType_algebraMap (A := R) (B := A.obj)).mpr A.2⟩
functor.map {A B} f := ⟨(commAlgCatEquivUnder R).functor.map f, trivial, trivial⟩
inverse.obj A := ⟨(commAlgCatEquivUnder R).inverse.obj A.1, A.2⟩
inverse.map {A B} f := (commAlgCatEquivUnder R).inverse.map f.hom
unitIso :=
NatIso.ofComponents fun A ↦
ObjectProperty.isoMk _ (CommAlgCat.isoMk { toRingEquiv := .refl A.1, commutes' _ := rfl })
counitIso := .refl _
