Theorems · Theorem · algebraic geometry

AlgebraicGeometry.HasRingHomProperty.stalkwise

∀ {P : {R S : Type u_1} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  RingHom.RespectsIso P →
    AlgebraicGeometry.HasRingHomProperty (AlgebraicGeometry.stalkwise fun {R S} [CommRing R] [CommRing S] => P)
      fun {x S} {x_1} {x_2} φ =>
      ∀ (p : Ideal S) (x_3 : p.IsPrime), P (Localization.localRingHom (Ideal.comap φ p) p φ ⋯)

Defined in

Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Cited by

0 results in Mathlib

Foundations

Depth 179 from the axioms · uses propext, Classical.choice, Quot.sound