Theorems · Theorem · algebraic geometry

AlgebraicGeometry.ExistsHomHomCompEqCompAux.range_g_subset

∀ {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),
  Set.range ⇑A.g ⊆ ↑(AlgebraicGeometry.Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X)

Defined in

Mathlib.AlgebraicGeometry.AffineTransitionLimit

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCompactSpaceCategoryTheory.IsCofilteredAlgebraicGeometry.IsAffineHom