Theorems · Theorem · algebraic geometry

AlgebraicGeometry.IsProper.of_comp

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

[Stacks Tag 01W6](https://stacks.math.columbia.edu/tag/01W6) ((2))

Defined in: Mathlib.AlgebraicGeometry.Morphisms.Proper
Cited by: 3 results in Mathlib
Foundations: Depth 226 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: AlgebraicGeometry.IsProper AlgebraicGeometry.IsSeparated

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites6

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
AlgebraicGeometry.IsSeparatedstatement and proof · cited by 31
CategoryTheory.MorphismProperty.of_postcompproof · cited by 17
AlgebraicGeometry.IsProperstatement and proof · cited by 17

Cited by3

Results whose statement or proof uses this declaration.

AlgebraicGeometry.exists_finite_imageι_comp_morphismRestrict_of_finite_image_preimageproof · cited by 1
AlgebraicGeometry.isCommMonObj_of_isProper_of_isIntegral_tensorObj_of_isAlgClosedproof · cited by 1
AlgebraicGeometry.IsProper.comp_iffproof · cited by 0