Module

smooth_isSeparated_quasiCompact_geometricallyConnected_of_finiteEtale_baseChange.lean

Nyll.AlgebraicCurves.Geometry.Curves.smooth_isSeparated_quasiCompact_geometricallyConnected_of_finiteEtale_baseChange

6 declarations indexed from sourceView source ↗

Module documentation

smooth is Separated quasi Compact geometrically Connected of finite Etale base Change

Imports13

Mathlib.AlgebraicGeometry.Geometrically.Connected
Mathlib.AlgebraicGeometry.Morphisms.Separated
Mathlib.AlgebraicGeometry.Morphisms.Immersion
Mathlib.AlgebraicGeometry.Morphisms.Finite
Mathlib.AlgebraicGeometry.Morphisms.Etale
Mathlib.AlgebraicGeometry.Morphisms.Smooth
Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
Mathlib.AlgebraicGeometry.PullbackCarrier
Mathlib.AlgebraicGeometry.ResidueField
Mathlib.RingTheory.RingHom.FaithfullyFlat
Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Nyll.AlgebraicCurves.Geometry.Schemes.Smooth_descendsAlong_surjective_inf_flat_inf_quasiCompact

Imported by2

theorem

isSeparated_iff_universallyClosed_diagonal

L59 ↗

AlgebraicCurves.Geometry.Curves.Proofs.smooth_isSeparated_quasiCompact_geometricallyConnected_of_finiteEtale_baseChange.AlgebraicGeometry.FiniteEtaleBaseChangeDescent'.isSeparated_iff_universallyClosed_diagonal

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace smooth_isSeparated_quasiCompact_geometricallyConnected_of_finiteEtale_baseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
attribute [local instance] _root_.AlgebraicGeometry.universallyClosed_respectsIso
namespace AlgebraicGeometry
namespace FiniteEtaleBaseChangeDescent'
open _root_.AlgebraicGeometry

Lean source · statement

theorem isSeparated_iff_universallyClosed_diagonal {X Y : Scheme.{u}} (f : X ⟶ Y) :
    IsSeparated f ↔ UniversallyClosed (pullback.diagonal f)

theorem

isSeparated_eq_diagonal_universallyClosed

L64 ↗

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace smooth_isSeparated_quasiCompact_geometricallyConnected_of_finiteEtale_baseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
attribute [local instance] _root_.AlgebraicGeometry.universallyClosed_respectsIso
namespace AlgebraicGeometry
namespace FiniteEtaleBaseChangeDescent'
open _root_.AlgebraicGeometry

Lean source · statement

theorem isSeparated_eq_diagonal_universallyClosed :
    @IsSeparated = MorphismProperty.diagonal (@UniversallyClosed : MorphismProperty Scheme.{u})

theorem

isSeparated_descendsAlong

L70 ↗

AlgebraicCurves.Geometry.Curves.Proofs.smooth_isSeparated_quasiCompact_geometricallyConnected_of_finiteEtale_baseChange.AlgebraicGeometry.FiniteEtaleBaseChangeDescent'.isSeparated_descendsAlong

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace smooth_isSeparated_quasiCompact_geometricallyConnected_of_finiteEtale_baseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
attribute [local instance] _root_.AlgebraicGeometry.universallyClosed_respectsIso
namespace AlgebraicGeometry
namespace FiniteEtaleBaseChangeDescent'
open _root_.AlgebraicGeometry

Lean source · statement

theorem isSeparated_descendsAlong :
    MorphismProperty.DescendsAlong (@IsSeparated : MorphismProperty Scheme.{u})
      (@Surjective ⊓ @Flat ⊓ @QuasiCompact)

theorem

quasiCompact_of_pullback_snd

L109 ↗

AlgebraicCurves.Geometry.Curves.Proofs.smooth_isSeparated_quasiCompact_geometricallyConnected_of_finiteEtale_baseChange.AlgebraicGeometry.FiniteEtaleBaseChangeDescent'.quasiCompact_of_pullback_snd

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace smooth_isSeparated_quasiCompact_geometricallyConnected_of_finiteEtale_baseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
attribute [local instance] _root_.AlgebraicGeometry.universallyClosed_respectsIso
namespace AlgebraicGeometry
namespace FiniteEtaleBaseChangeDescent'
open _root_.AlgebraicGeometry

Lean source · statement

theorem quasiCompact_of_pullback_snd {X S S' : Scheme.{u}} (f : X ⟶ S) (σ : S' ⟶ S) [Surjective σ]
    [QuasiCompact σ] [hq : QuasiCompact (pullback.snd f σ)] : QuasiCompact f

theorem

geometricallyConnected_of_pullback_snd

L133 ↗

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace smooth_isSeparated_quasiCompact_geometricallyConnected_of_finiteEtale_baseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
attribute [local instance] _root_.AlgebraicGeometry.universallyClosed_respectsIso
namespace AlgebraicGeometry
namespace FiniteEtaleBaseChangeDescent'
open _root_.AlgebraicGeometry

Lean source · statement

theorem geometricallyConnected_of_pullback_snd {X S S' : Scheme.{u}} (f : X ⟶ S) (σ : S' ⟶ S)
  [Surjective σ]
    [hgc : GeometricallyConnected (pullback.snd f σ)] : GeometricallyConnected f

theorem

smooth_isSeparated_quasiCompact_geometricallyConnected_of_finiteEtale_baseChange

L172 ↗

AlgebraicGeometry.smooth_isSeparated_quasiCompact_geometricallyConnected_of_finiteEtale_baseChange

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicGeometry
universe u
open _root_.CategoryTheory _root_.CategoryTheory.Limits _root_.AlgebraicGeometry
attribute [local instance] _root_.AlgebraicGeometry.universallyClosed_respectsIso
open _root_.AlgebraicCurves.Geometry.Curves.Proofs in
open smooth_isSeparated_quasiCompact_geometricallyConnected_of_finiteEtale_baseChange in

Lean source · statement

theorem smooth_isSeparated_quasiCompact_geometricallyConnected_of_finiteEtale_baseChange
    (R : Type u) [CommRing R] (R' : Type u) [CommRing R'] [Algebra R R'] [Module.Finite R R']
    [Algebra.Etale R R'] [Module.FaithfullyFlat R R']
    {X : AlgebraicGeometry.Scheme.{u}} (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of R))
    {X' : AlgebraicGeometry.Scheme.{u}} (x' : X' ⟶ AlgebraicGeometry.Spec (CommRingCat.of R'))
    (hsm : AlgebraicGeometry.Smooth x') (hsep : AlgebraicGeometry.IsSeparated x') (hqc :
      AlgebraicGeometry.QuasiCompact x')
    (hgc : AlgebraicGeometry.GeometricallyConnected x')
    (e : CategoryTheory.Limits.pullback f (AlgebraicGeometry.Spec.map (CommRingCat.ofHom
      (algebraMap R R'))) ≅ X')
    (he : e.hom ≫ x' = CategoryTheory.Limits.pullback.snd f (AlgebraicGeometry.Spec.map
      (CommRingCat.ofHom (algebraMap R R')))) :
    AlgebraicGeometry.Smooth f ∧ AlgebraicGeometry.IsSeparated f ∧ AlgebraicGeometry.QuasiCompact f
      ∧
      AlgebraicGeometry.GeometricallyConnected f

Module documentation

smooth is Separated quasi Compact geometrically Connected of finite Etale base Change

Declarations

isSeparated_iff_universallyClosed_diagonal

isSeparated_eq_diagonal_universallyClosed

isSeparated_descendsAlong

quasiCompact_of_pullback_snd

geometricallyConnected_of_pullback_snd

smooth_isSeparated_quasiCompact_geometricallyConnected_of_finiteEtale_baseChange