Theorems · Theorem · algebraic geometry

AlgebraicGeometry.UniversallyClosed.of_comp_surjective

∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z)
  [AlgebraicGeometry.UniversallyClosed (CategoryTheory.CategoryStruct.comp f g)] [AlgebraicGeometry.Surjective f],
  AlgebraicGeometry.UniversallyClosed g

Defined in: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
Cited by: 2 results in Mathlib
Foundations: Depth 194 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: AlgebraicGeometry.UniversallyClosed AlgebraicGeometry.Surjective

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites17

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Quiver.Homstatement and proof · cited by 32,603
CategoryTheory.CategoryStruct.compstatement and proof · cited by 17,999
AlgebraicGeometry.Schemestatement and proof · cited by 2,540
CategoryTheory.Limits.pullbackproof · cited by 864
CategoryTheory.Limits.pullback.fstproof · cited by 639
CategoryTheory.Limits.pullback.sndproof · cited by 637
CategoryTheory.IsPullbackproof · cited by 320
IsClosedMapproof · cited by 138
CategoryTheory.IsPullback.of_hasPullbackproof · cited by 70
AlgebraicGeometry.Surjectivestatement and proof · cited by 48
AlgebraicGeometry.Scheme.Hom.continuousproof · cited by 41
AlgebraicGeometry.topologicallyproof · cited by 35

Cited by2

Results whose statement or proof uses this declaration.

AlgebraicGeometry.exists_finite_imageι_comp_morphismRestrict_of_finite_image_preimageproof · cited by 1
AlgebraicGeometry.isIntegral_appTop_of_universallyClosedproof · cited by 1