Theorems · Inductive type · algebraic geometry

AlgebraicGeometry.HasRingHomProperty

CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme →
  outParam ({R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) → Prop

HasRingHomProperty P Q is a type class asserting that P is local at the target and the source, and for f : Spec B ⟶ Spec A, it is equivalent to the ring hom property Q. To make the proofs easier, we state it instead as 1. Q is local (See RingHom.PropertyIsLocal) 2. P f if and only if Q holds for every Γ(Y, U) ⟶ Γ(X, V) for all affine U, V. See HasRingHomProperty.iff_appLE.

Defined in

Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Cited by

38 results in Mathlib

Foundations

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