Binary coproducts of finite morphisms #
Schemes with a finite morphism to a fixed scheme X are closed under binary coproducts: if
f : U ⟶ X and g : V ⟶ X are finite, then so is coprod.desc f g : U ⨿ V ⟶ X.
AlgebraicGeometry.IsFinite.isClosedUnderColimitsOfShape_walkingPair states this as closure of
MorphismProperty.costructuredArrowObj L @IsFinite under binary coproducts, in the shape of
Mathlib's AlgebraicGeometry.IsZariskiLocalAtSource.isClosedUnderColimitsOfShape_discrete. The
finiteness of coprod.desc f g is Mathlib's instance in
Mathlib.AlgebraicGeometry.Morphisms.Finite.
instance
AlgebraicGeometry.IsFinite.isClosedUnderColimitsOfShape_walkingPair
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C]
(L : CategoryTheory.Functor C Scheme)
[CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) L]
(X : Scheme)
:
Objects of CostructuredArrow L X whose structure morphism is finite are closed under binary
coproducts.