ofSurjectiveAlgebraMap — Mathlib

English

The canonical Generators for the base ring R acting as R-algebra on itself is constructed via the ofSurjectiveAlgebraMap applied to the identity map, i.e., the R-algebra of R generated by nothing beyond the trivial map.

Русский

Канонические Генераторы для основы R, действующие как R-алгебра над самим R, строятся через ofSurjectiveAlgebraMap на тождественном отображении.

LaTeX

$$self : Generators R R PEmpty$$

Lean4

/-- If `algebraMap R S` is surjective, the empty type generates `S`. -/
noncomputable def ofSurjectiveAlgebraMap (h : Function.Surjective (algebraMap R S)) : Generators R S PEmpty.{w + 1} :=
  ofSurjective PEmpty.elim <| fun s ↦ by
    use C (h s).choose
    simp [(h s).choose_spec]

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