pullback_fst_appTop — Mathlib

English

Define a property of ring homomorphisms P to be affine-locally satisfied if for every affine open U ⊆ Y and V ⊆ f⁻¹(U) the induced map of rings has P.

Русский

Определение: свойство P подграно через аффинные открытые; на каждом аффинном открытом U ⊆ Y и соответствующем V ⊆ f⁻¹(U) свойство P выполняется для соответствующей гомоморфизмы колец.

LaTeX

$$affineLocally P := ∀ U ∈ Y.affineOpens, P (f.appLE ⊤ U le_top).hom$$

Lean4

theorem pullback_fst_appTop (hP : IsStableUnderBaseChange P) (hP' : RespectsIso P) {X Y S : Scheme} [IsAffine X]
    [IsAffine Y] [IsAffine S] (f : X ⟶ S) (g : Y ⟶ S) (H : P g.appTop.hom) : P (pullback.fst f g).appTop.hom := by
  -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11224): change `rw` to `erw`

  erw [← PreservesPullback.iso_inv_fst AffineScheme.forgetToScheme (AffineScheme.ofHom f) (AffineScheme.ofHom g)]
  rw [Scheme.comp_appTop, CommRingCat.hom_comp, hP'.cancel_right_isIso, AffineScheme.forgetToScheme_map]
  have :=
    congr_arg Quiver.Hom.unop
      (PreservesPullback.iso_hom_fst AffineScheme.Γ.rightOp (AffineScheme.ofHom f) (AffineScheme.ofHom g))
  simp only [AffineScheme.Γ, Functor.rightOp_obj, Functor.comp_obj, Functor.op_obj, unop_comp,
    AffineScheme.forgetToScheme_obj, Scheme.Γ_obj, Functor.rightOp_map, Functor.comp_map, Functor.op_map,
    Quiver.Hom.unop_op, AffineScheme.forgetToScheme_map, Scheme.Γ_map] at this
  rw [← this, CommRingCat.hom_comp, hP'.cancel_right_isIso, ← pushoutIsoUnopPullback_inl_hom, CommRingCat.hom_comp,
    hP'.cancel_right_isIso]
  exact hP.pushout_inl hP' _ _ H

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