fromGens_coe — Mathlib

English

If two DividedPowers structures on I and J agree on a generating set, then the transport construction from gens yields equality of the induced ring homomorphisms.

Русский

Если две структуры делённых степеней на I и J совпадают на наборе порождающих, то перенос по порождающим даёт равенство соответствующих кольцевых гомоморфизмов.

LaTeX

$$$\\text{fromGens } hI\\; hJ\\; hS\\; hf$ induces equality on the transported dpow maps.$$

Lean4

theorem fromGens_coe {f : A →+* B} {S : Set A} (hS : I = span S) (hf : I.map f ≤ J)
    (h : ∀ {n : ℕ}, ∀ x ∈ S, f (hI.dpow n x) = hJ.dpow n (f x)) : (fromGens hI hJ hS hf h).toRingHom = f :=
  rfl

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