ofBijectiveAlgebraMap — Mathlib

English

If the algebra map R → S is bijective, the empty generators form a submersive presentation of R over S with no relations.

Русский

Если отображение алгебры R → S биективно, то пустые генераторы дают подмассовое представление R над S без ограничений.

LaTeX

$$$\\text{ofBijectiveAlgebraMap}(h) : \\text{SubmersivePresentation } R S PEmpty PEmpty$, where $h$ is a bijection between the rings.$$

Lean4

/-- If `algebraMap R S` is bijective, the empty generators are a submersive
presentation with no relations. -/
noncomputable def ofBijectiveAlgebraMap (h : Function.Bijective (algebraMap R S)) :
    SubmersivePresentation R S PEmpty.{w + 1} PEmpty.{t + 1}
    where
  __ := PreSubmersivePresentation.ofBijectiveAlgebraMap.{t, w} h
  jacobian_isUnit := by
    rw [ofBijectiveAlgebraMap_jacobian]
    exact isUnit_one

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