of_ringHom_of_comp_eq — Mathlib

English

If f, g satisfy a composition equality and certain algebraicity assumptions hold, then IsAlgebraic S B holds given IsAlgebraic R A.

Русский

Если f, g удовлетворяют равенству композиции и выполняются условия алгебраичности, то IsAlgebraic S B следует из IsAlgebraic R A.

LaTeX

$$$\text{IsAlgebraic}(R, A) \Rightarrow \text{IsAlgebraic}(S, B)$ при равенстве композиции.$$

Lean4

theorem of_ringHom_of_comp_eq [Algebra.IsAlgebraic S B] (hf : Function.Surjective f) (hg : Function.Injective g)
    (h : RingHom.comp (algebraMap S B) f = RingHom.comp g (algebraMap R A)) : Algebra.IsAlgebraic R A :=
  ⟨fun a ↦ (Algebra.IsAlgebraic.isAlgebraic (g a)).of_ringHom_of_comp_eq f g hf hg h⟩

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