isoSpec_inv_naturality — Mathlib

English

Dually, the inverse isoSpec maps satisfy a naturality relation with respect to f: Spec.map(f.top) then Y.isoSpec.inv equals X.isoSpec.inv then f.

Русский

С другой стороны, обратная естественная связь isoSpec удовлетворяет тождественности: Spec.map(f.appTop) ; Y.isoSpec.inv = X.isoSpec.inv ; f.

LaTeX

$$$\\mathrm{Spec.map}(f_{\\mathrm{top}}) \\;\\circ\\; Y.isoSpec.inv = X.isoSpec.inv \\;\\circ\\; f$$$

Lean4

@[reassoc]
theorem isoSpec_inv_naturality {X Y : Scheme} [IsAffine X] [IsAffine Y] (f : X ⟶ Y) :
    Spec.map (f.appTop) ≫ Y.isoSpec.inv = X.isoSpec.inv ≫ f := by
  rw [Iso.eq_inv_comp, isoSpec, asIso_hom, ← Scheme.toSpecΓ_naturality_assoc, isoSpec, asIso_inv, IsIso.hom_inv_id,
    Category.comp_id]

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