map_of_comp_eq — Mathlib

English

Assume φ and ψ are ring homomorphisms with a commutativity condition on their compositions; integrality is preserved along ψ.

Русский

Пусть есть гомоморфизмы φ и ψ такие, что композиции удовлетворяют условию; интеграленость сохраняется по ψ.

LaTeX

$$$\\text{IsIntegral}_T(\\psi(a))\\leftarrow\\text{IsIntegral}_R(a)$ при условии равенства композиций$$

Lean4

theorem map_of_comp_eq {R S T U : Type*} [CommRing R] [Ring S] [CommRing T] [Ring U] [Algebra R S] [Algebra T U]
    (φ : R →+* T) (ψ : S →+* U) (h : (algebraMap T U).comp φ = ψ.comp (algebraMap R S)) {a : S} (ha : IsIntegral R a) :
    IsIntegral T (ψ a) :=
  let ⟨p, hp⟩ := ha
  ⟨p.map φ, hp.1.map _, by rw [← eval_map, map_map, h, ← map_map, eval_map, eval₂_at_apply, eval_map, hp.2, ψ.map_zero]⟩

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