Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.Hom.liftQuotient_comp_assoc

∀ {X : AlgebraicGeometry.Scheme} {A : CommRingCat} (f : X.Hom (AlgebraicGeometry.Spec A)) (I : Ideal ↑A)
  (hI :
    I ≤
      RingHom.ker
        (CommRingCat.Hom.hom (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso A).inv f.appTop)))
  {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec (CommRingCat.of ↑A) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (f.liftQuotient I hI)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))) h) =
    CategoryTheory.CategoryStruct.comp f h

Defined in

Mathlib.AlgebraicGeometry.AffineScheme

Cited by

1 results in Mathlib

Foundations

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