Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.Hom.liftQuotient

{X : AlgebraicGeometry.Scheme} →
  {A : CommRingCat} →
    (f : X.Hom (AlgebraicGeometry.Spec A)) →
      (I : Ideal ↑A) →
        I ≤
            RingHom.ker
              (CommRingCat.Hom.hom
                (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso A).inv f.appTop)) →
          (X ⟶ AlgebraicGeometry.Spec (CommRingCat.of (↑A ⧸ I)))

Given f : X ⟶ Spec A and some ideal I ≤ ker(A ⟶ Γ(X, ⊤)), this is the lift to X ⟶ Spec (A ⧸ I).

Defined in

Mathlib.AlgebraicGeometry.AffineScheme

Cited by

4 results in Mathlib

Foundations

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