English
If the algebra map algebraMap R S is bijective, there exists a presentation of S over R with no generators and no relations.
Русский
Если отображение алгебра-мэппинг R в S биективно, существует презентация S над R без генераторов и без реляций.
LaTeX
$$$\\exists h\\ :\\ Function.Bijective(\\mathrm{algebraMap}\\ R\\ S)\\;\\to\\;\\mathrm{Presentation}\\; R\\ S\\; \\mathrm{PEmpty}\\; \\mathrm{PEmpty}$$$
Lean4
/-- If `algebraMap R S` is bijective, the empty generators are a presentation with no relations. -/
noncomputable def ofBijectiveAlgebraMap (h : Function.Bijective (algebraMap R S)) :
Presentation R S PEmpty.{w + 1} PEmpty.{t + 1}
where
__ := Generators.ofSurjectiveAlgebraMap h.surjective
relation := PEmpty.elim
span_range_relation_eq_ker := by
simp only [Set.range_eq_empty, Ideal.span_empty]
symm
rw [← RingHom.injective_iff_ker_eq_bot]
change Function.Injective (aeval PEmpty.elim)
rw [aeval_injective_iff_of_isEmpty]
exact h.injective
