Module

Smooth_descendsAlong_surjective_inf_flat_inf_quasiCompact.lean

Nyll.AlgebraicCurves.Geometry.Schemes.Smooth_descendsAlong_surjective_inf_flat_inf_quasiCompact

2 declarations indexed from sourceView source ↗

Module documentation

Smooth descends Along surjective inf flat inf quasi Compact

Imports3

Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Mathlib.AlgebraicGeometry.Morphisms.Smooth
Mathlib.RingTheory.Etale.Descent

Imported by4

theorem

desc_smooth_descendsAlong

L37 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Smooth_descendsAlong_surjective_inf_flat_inf_quasiCompact.AlgebraicGeometry.desc_smooth_descendsAlong

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Smooth_descendsAlong_surjective_inf_flat_inf_quasiCompact
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MorphismProperty
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry

Lean source · full declaration

theorem desc_smooth_descendsAlong :
    DescendsAlong ((fun {X Y : Scheme.{u}} (h : X ⟶ Y) => Smooth h) : MorphismProperty Scheme.{u})
      ((fun {X Y : Scheme.{u}} (h : X ⟶ Y) => Surjective h) ⊓ (fun {X Y : Scheme.{u}} (h : X ⟶ Y)
        => Flat h) ⊓ (fun {X Y : Scheme.{u}} (h : X ⟶ Y) => QuasiCompact h)) := by
  have : MorphismProperty.IsStableUnderBaseChange
      (fun {X Y : Scheme.{u}} (h : X ⟶ Y) => Smooth h) :=
    smooth_isStableUnderBaseChange
  exact HasRingHomProperty.descendsAlong_flat
    (P := fun {X Y : Scheme.{u}} (h : X ⟶ Y) => Smooth h)
    (Q := RingHom.Smooth) RingHom.Smooth.codescendsAlong_faithfullyFlat

theorem

descendsAlong_surjective_inf_flat_inf_quasiCompact

L52 ↗

AlgebraicGeometry.Smooth.descendsAlong_surjective_inf_flat_inf_quasiCompact

Source context 8 commands