NYLL
Module

smooth_isProper_geometricallyConnected_of_finiteEtale_baseChange.lean

Nyll.AlgebraicCurves.Geometry.Curves.smooth_isProper_geometricallyConnected_of_finiteEtale_baseChange
7 declarations indexed from sourceView source ↗

Module documentation

smooth is Proper geometrically Connected of finite Etale base Change

Imports7
Imported by3

Declarations

theorem

locallyOfFiniteType_descendsAlong

L41 ↗
AlgebraicCurves.Geometry.Curves.Proofs.smooth_isProper_geometricallyConnected_of_finiteEtale_baseChange.AlgebraicGeometry.FiniteEtaleBaseChangeDescent.locallyOfFiniteType_descendsAlong
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace smooth_isProper_geometricallyConnected_of_finiteEtale_baseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace FiniteEtaleBaseChangeDescent
open _root_.AlgebraicGeometry
Lean source · statement
theorem locallyOfFiniteType_descendsAlong :
    MorphismProperty.DescendsAlong (@LocallyOfFiniteType : MorphismProperty Scheme.{u})
      (@Surjective ⊓ @Flat ⊓ @QuasiCompact)
theorem

isSeparated_iff_universallyClosed_diagonal

L51 ↗
AlgebraicCurves.Geometry.Curves.Proofs.smooth_isProper_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_isProper_geometricallyConnected_of_finiteEtale_baseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.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

L56 ↗
AlgebraicCurves.Geometry.Curves.Proofs.smooth_isProper_geometricallyConnected_of_finiteEtale_baseChange.AlgebraicGeometry.FiniteEtaleBaseChangeDescent.isSeparated_eq_diagonal_universallyClosed
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace smooth_isProper_geometricallyConnected_of_finiteEtale_baseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace FiniteEtaleBaseChangeDescent
open _root_.AlgebraicGeometry
Lean source · statement
theorem isSeparated_eq_diagonal_universallyClosed :
    @IsSeparated = MorphismProperty.diagonal (@UniversallyClosed : MorphismProperty Scheme.{u})
theorem

isSeparated_descendsAlong

L63 ↗
AlgebraicCurves.Geometry.Curves.Proofs.smooth_isProper_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_isProper_geometricallyConnected_of_finiteEtale_baseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace FiniteEtaleBaseChangeDescent
open _root_.AlgebraicGeometry
Lean source · statement
theorem isSeparated_descendsAlong :
    MorphismProperty.DescendsAlong (@IsSeparated : MorphismProperty Scheme.{u})
      (@Surjective ⊓ @Flat ⊓ @QuasiCompact)
theorem

isProper_descendsAlong

L98 ↗
AlgebraicCurves.Geometry.Curves.Proofs.smooth_isProper_geometricallyConnected_of_finiteEtale_baseChange.AlgebraicGeometry.FiniteEtaleBaseChangeDescent.isProper_descendsAlong
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace smooth_isProper_geometricallyConnected_of_finiteEtale_baseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace FiniteEtaleBaseChangeDescent
open _root_.AlgebraicGeometry
Lean source · statement
theorem isProper_descendsAlong :
    MorphismProperty.DescendsAlong (@IsProper : MorphismProperty Scheme.{u})
      (@Surjective ⊓ @Flat ⊓ @QuasiCompact)
theorem

geometricallyConnected_of_pullback_snd

L114 ↗
AlgebraicCurves.Geometry.Curves.Proofs.smooth_isProper_geometricallyConnected_of_finiteEtale_baseChange.AlgebraicGeometry.FiniteEtaleBaseChangeDescent.geometricallyConnected_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_isProper_geometricallyConnected_of_finiteEtale_baseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.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_isProper_geometricallyConnected_of_finiteEtale_baseChange

L142 ↗
AlgebraicGeometry.smooth_isProper_geometricallyConnected_of_finiteEtale_baseChange
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace smooth_isProper_geometricallyConnected_of_finiteEtale_baseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open AlgebraicGeometry.FiniteEtaleBaseChangeDescent in
Lean source · statement
theorem _root_.AlgebraicGeometry.smooth_isProper_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 : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of R)) {X' : Scheme.{u}} (x' : X' ⟶ Spec
      (CommRingCat.of R'))
    (hsm : Smooth x') (hpr : IsProper x') (hgc : GeometricallyConnected x')
    (e : pullback f (Spec.map (CommRingCat.ofHom (algebraMap R R'))) ≅ X')
    (he : e.hom ≫ x' = pullback.snd f (Spec.map (CommRingCat.ofHom (algebraMap R R')))) :
    Smooth f ∧ IsProper f ∧ GeometricallyConnected f

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.