copy — Mathlib

English

Properties preserved under isomorphism transfer along equality of properties.

Русский

Свойства, сохраняемые при изоморфизмах, переносятся по равенству свойств.

LaTeX

$$HasRingHomProperty P' Q' from P = P'$$

Lean4

theorem copy {P' : MorphismProperty Scheme.{u}} {Q' : ∀ {R S : Type u} [CommRing R] [CommRing S], (R →+* S) → Prop}
    (e : P = P') (e' : ∀ {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S), Q f ↔ Q' f) :
    HasRingHomProperty P' Q' := by
  subst e
  have heq : @Q = @Q' := by
    ext R S _ _ f
    exact (e' f)
  rw [← heq]
  infer_instance

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