isLocal_ringHomProperty_of_isZariskiLocalAtSource_of_isZariskiLocalAtTarget

English

Between ring-theoretic and scheme-theoretic properties, Spec map preserves the equivalence of P and Q.

Русский

Между кольцевыми и схематическими свойствами карта Spec сохраняет эквивалентность P и Q.

LaTeX

$$Spec_iff$$

Lean4

theorem isLocal_ringHomProperty_of_isZariskiLocalAtSource_of_isZariskiLocalAtTarget [IsZariskiLocalAtTarget P]
    [IsZariskiLocalAtSource P] : RingHom.PropertyIsLocal fun f ↦ P (Spec.map (CommRingCat.ofHom f)) :=
  by
  have hP : RingHom.RespectsIso (fun f ↦ P (Spec.map (CommRingCat.ofHom f))) :=
    RingHom.toMorphismProperty_respectsIso_iff.mpr (inferInstanceAs (P.inverseImage Scheme.Spec).unop.RespectsIso)
  constructor
  · intro R S _ _ f r R' S' _ _ _ _ _ _ H
    refine (RingHom.RespectsIso.isLocalization_away_iff hP ..).mp ?_
    exact
      (MorphismProperty.arrow_mk_iso_iff P (SpecMapRestrictBasicOpenIso (CommRingCat.ofHom f) r)).mp
        (IsZariskiLocalAtTarget.restrict H (basicOpen r))
  · intro R S _ _ f s hs H
    apply
      IsZariskiLocalAtSource.of_openCover
        (Scheme.affineOpenCoverOfSpanRangeEqTop (fun i : s ↦ (i : S)) (by simpa)).openCover
    intro i
    simp only [CommRingCat.coe_of, Scheme.AffineOpenCover.openCover_X, ← Spec.map_comp,
      Scheme.AffineOpenCover.openCover_f, Scheme.affineOpenCoverOfSpanRangeEqTop_f]
    exact H i
  · intro R S _ _ f s hs H
    apply
      IsZariskiLocalAtTarget.of_iSup_eq_top _
        (PrimeSpectrum.iSup_basicOpen_eq_top_iff (f := fun i : s ↦ (i : R)).mpr (by simpa))
    intro i
    exact (MorphismProperty.arrow_mk_iso_iff P (SpecMapRestrictBasicOpenIso (CommRingCat.ofHom f) i.1)).mpr (H i)
  · intro R S T _ _ _ _ r _ f hf
    have := AlgebraicGeometry.IsOpenImmersion.of_isLocalization (S := T) r
    change P (Spec.map (CommRingCat.ofHom f ≫ CommRingCat.ofHom (algebraMap _ _)))
    rw [Spec.map_comp]
    exact IsZariskiLocalAtSource.comp hf ..

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