Theorems · Definition · algebraic geometry

AlgebraicGeometry.ExistsHomHomCompEqCompAux.g

{I : Type u} →
  [inst : CategoryTheory.Category.{u, u} I] →
    {S X : AlgebraicGeometry.Scheme} →
      {D : CategoryTheory.Functor I AlgebraicGeometry.Scheme} →
        {t : D ⟶ (CategoryTheory.Functor.const I).obj S} →
          {f : X ⟶ S} →
            [inst_1 : ∀ (i : I), CompactSpace ↥(D.obj i)] →
              [inst_2 : CategoryTheory.IsCofiltered I] →
                [inst_3 : ∀ {i j : I} (f : i ⟶ j), AlgebraicGeometry.IsAffineHom (D.map f)] →
                  (A : AlgebraicGeometry.ExistsHomHomCompEqCompAux D t f) →
                    D.obj A.i' ⟶ CategoryTheory.Limits.pullback f f

(Implementation) The map sending x to (a x, b x), which should fall in the diagonal component. See the section docstring.

Defined in

Mathlib.AlgebraicGeometry.AffineTransitionLimit

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCompactSpaceCategoryTheory.IsCofilteredAlgebraicGeometry.IsAffineHom