This file proves the finite-coproduct part of Stacks Project, Tag 0BNA, directly for the canonical forgetful functor from finite étale schemes.
Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public section
noncomputable section
universe u v
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
variable (X : Scheme.{u})instance : IsZariskiLocalAtSource
(@Etale : MorphismProperty Scheme.{u})Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public section
noncomputable section
universe u v
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
variable (X : Scheme.{u})instance : MorphismProperty.RespectsIso
(@IsFiniteEtale : MorphismProperty Scheme.{u})Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public section
noncomputable section
universe u v
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
variable (X : Scheme.{u})lemma isFiniteEtale_sigmaDesc_walkingPair {T : Scheme.{u}}
(Y : WalkingPair → Scheme.{u})
(f : ∀ i, Y i ⟶ T) (hf : ∀ i, IsFiniteEtale (f i)) :
IsFiniteEtale (Sigma.desc f)Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public section
noncomputable section
universe u v
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
variable (X : Scheme.{u})lemma isFiniteEtale_sigmaDesc_empty {T : Scheme.{u}}
(Y : PEmpty.{v + 1} → Scheme.{u}) [Small.{u} PEmpty.{v + 1}]
(f : ∀ i, Y i ⟶ T) :
IsFiniteEtale (Sigma.desc f)Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public section
noncomputable section
universe u v
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
variable (X : Scheme.{u})instance isClosedUnderBinaryCoproducts (X : Scheme.{u}) :
ObjectProperty.IsClosedUnderColimitsOfShape
(MorphismProperty.costructuredArrowObj
(𝟭 Scheme.{u}) (X := X) (@IsFiniteEtale))
(Discrete WalkingPair)Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public section
noncomputable section
universe u v
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
variable (X : Scheme.{u})instance isClosedUnderInitial (X : Scheme.{u}) :
ObjectProperty.IsClosedUnderColimitsOfShape
(MorphismProperty.costructuredArrowObj
(𝟭 Scheme.{u}) (X := X) (@IsFiniteEtale))
(Discrete PEmpty.{1})Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public section
noncomputable section
universe u v
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
variable (X : Scheme.{u})instance isClosedUnderBinaryCoproductsComma (X : Scheme.{u}) :
ObjectProperty.IsClosedUnderColimitsOfShape
(MorphismProperty.commaObj (𝟭 Scheme.{u}) (Functor.fromPUnit.{0} X)
(@IsFiniteEtale))
(Discrete WalkingPair)Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public section
noncomputable section
universe u v
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
variable (X : Scheme.{u})instance isClosedUnderInitialComma (X : Scheme.{u}) :
ObjectProperty.IsClosedUnderColimitsOfShape
(MorphismProperty.commaObj (𝟭 Scheme.{u}) (Functor.fromPUnit.{0} X)
(@IsFiniteEtale))
(Discrete PEmpty.{1})Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public section
noncomputable section
universe u v
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
variable (X : Scheme.{u})instance forgetCreatesBinaryCoproducts :
CreatesColimitsOfShape (Discrete WalkingPair) (forget X)Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public section
noncomputable section
universe u v
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
variable (X : Scheme.{u})instance forgetCreatesInitial :
CreatesColimitsOfShape (Discrete PEmpty.{1}) (forget X)Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public section
noncomputable section
universe u v
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
variable (X : Scheme.{u})instance forgetPreservesBinaryCoproducts :
PreservesColimitsOfShape (Discrete WalkingPair) (forget X)Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public section
noncomputable section
universe u v
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
variable (X : Scheme.{u})instance forgetPreservesInitial :
PreservesColimitsOfShape (Discrete PEmpty.{1}) (forget X)The canonical forgetful functor from finite étale schemes over X to schemes over X preserves finite coproducts.
Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public section
noncomputable section
universe u v
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
variable (X : Scheme.{u})instance forgetPreservesFiniteCoproducts :
PreservesFiniteCoproducts (forget X) where
preserves n := PreservesFiniteCoproducts.of_preserves_binary_and_initial (forget X) (Fin n)Forgetting a finite étale scheme all the way to schemes preserves finite coproducts.
Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public section
noncomputable section
universe u v
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
variable (X : Scheme.{u})instance forgetCompOverForgetPreservesFiniteCoproducts :
PreservesFiniteCoproducts (forget X ⋙ CategoryTheory.Over.forget X)