NYLL
Module

exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_opensRestrict_pullback_snd.lean

Nyll.AlgebraicCurves.Geometry.Schemes.exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_opensRestrict_pullback_snd
4 declarations indexed from sourceView source ↗

Module documentation

exists mem and smooth Of Relative Dimension one of smooth Of Relative Dimension opens

Restrict pullback snd

Imports24
Imported by1

Declarations

theorem

eq_of_locally_isStandardSmoothOfRelativeDimension

L97 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.SmoothRestrictedPullbackDescent.AlgebraicGeometry.FibreCritPt.eq_of_locally_isStandardSmoothOfRelativeDimension
Source context 12 commands

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

section ProofImplementation
open _root_.AlgebraicGeometry.Scheme.Hom (
  fiberInclusion_mem_smoothLocus_of_mem_smoothLocus_fiberToSpecResidueField)
namespace AlgebraicCurves.Geometry.Schemes.Proofs.SmoothRestrictedPullbackDescent
attribute [-instance] TwoChartCech.Sections.M0_moduleA TwoChartCech.Sections.M1_module
  TwoChartCech.Cover.A01_algebra TwoChartCech.Cover.A0_algebra TwoChartCech.Cover.A1_commRing
  TwoChartCech.Cover.A1_algebra TwoChartCech.Sections.M01_module
  TwoChartCech.Sections.M0_addCommGroup TwoChartCech.Sections.M0_tower
  TwoChartCech.Sections.M01_addCommGroup TwoChartCech.Cover.A0_commRing
  TwoChartCech.Sections.M1_tower TwoChartCech.Sections.M01_moduleA TwoChartCech.Sections.M0_module
  TwoChartCech.Sections.M1_moduleA TwoChartCech.Sections.M1_addCommGroup
  TwoChartCech.Cover.A01_commRing TwoChartCech.Sections.M01_tower
  CoherentBaseChange.TwoTermComplex.C0_module CoherentBaseChange.TwoTermComplex.C0_addCommGroup
  CoherentBaseChange.TwoTermComplex.C1_module CoherentBaseChange.TwoTermComplex.C1_addCommGroup
  CoherentBaseChange.TwoTermComplex.C0_free CoherentBaseChange.TwoTermComplex.C1_finite
  CoherentBaseChange.TwoTermComplex.C0_finite CoherentBaseChange.TwoTermComplex.C1_free
attribute [-simp] AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.injEq
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U1
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U0 TwoChartCech.Sections.mk.injEq
  TwoChartCech.Cover.mk.injEq TwoChartCech.GrothendieckComplex.mk.injEq
  TwoChartCech.Sections.mk.sizeOf_spec TwoChartCech.Cover.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r0_apply TwoChartCech.GrothendieckComplex.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r1_apply CoherentBaseChange.TwoTermComplex.mk.sizeOf_spec
  CoherentBaseChange.TwoTermComplex.mk.injEq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
namespace FibreCritPt
open _root_.AlgebraicGeometry
Lean source · statement
theorem eq_of_locally_isStandardSmoothOfRelativeDimension {R S : Type u} [CommRing R] [CommRing S]
    (f : R →+* S) {n m : ℕ} (hn : RingHom.Locally (RingHom.IsStandardSmoothOfRelativeDimension n) f)
    (hm : RingHom.Locally (RingHom.IsStandardSmoothOfRelativeDimension m) f)
    (Q : Ideal S) [Q.IsPrime] : n = m
theorem

eq_of_nonempty

L152 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.SmoothRestrictedPullbackDescent.AlgebraicGeometry.FibreCritPt.SmoothOfRelativeDimension.eq_of_nonempty
Source context 12 commands

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

section ProofImplementation
open _root_.AlgebraicGeometry.Scheme.Hom (
  fiberInclusion_mem_smoothLocus_of_mem_smoothLocus_fiberToSpecResidueField)
namespace AlgebraicCurves.Geometry.Schemes.Proofs.SmoothRestrictedPullbackDescent
attribute [-instance] TwoChartCech.Sections.M0_moduleA TwoChartCech.Sections.M1_module
  TwoChartCech.Cover.A01_algebra TwoChartCech.Cover.A0_algebra TwoChartCech.Cover.A1_commRing
  TwoChartCech.Cover.A1_algebra TwoChartCech.Sections.M01_module
  TwoChartCech.Sections.M0_addCommGroup TwoChartCech.Sections.M0_tower
  TwoChartCech.Sections.M01_addCommGroup TwoChartCech.Cover.A0_commRing
  TwoChartCech.Sections.M1_tower TwoChartCech.Sections.M01_moduleA TwoChartCech.Sections.M0_module
  TwoChartCech.Sections.M1_moduleA TwoChartCech.Sections.M1_addCommGroup
  TwoChartCech.Cover.A01_commRing TwoChartCech.Sections.M01_tower
  CoherentBaseChange.TwoTermComplex.C0_module CoherentBaseChange.TwoTermComplex.C0_addCommGroup
  CoherentBaseChange.TwoTermComplex.C1_module CoherentBaseChange.TwoTermComplex.C1_addCommGroup
  CoherentBaseChange.TwoTermComplex.C0_free CoherentBaseChange.TwoTermComplex.C1_finite
  CoherentBaseChange.TwoTermComplex.C0_finite CoherentBaseChange.TwoTermComplex.C1_free
attribute [-simp] AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.injEq
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U1
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U0 TwoChartCech.Sections.mk.injEq
  TwoChartCech.Cover.mk.injEq TwoChartCech.GrothendieckComplex.mk.injEq
  TwoChartCech.Sections.mk.sizeOf_spec TwoChartCech.Cover.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r0_apply TwoChartCech.GrothendieckComplex.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r1_apply CoherentBaseChange.TwoTermComplex.mk.sizeOf_spec
  CoherentBaseChange.TwoTermComplex.mk.injEq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
namespace FibreCritPt
open _root_.AlgebraicGeometry
Lean source · statement
theorem SmoothOfRelativeDimension.eq_of_nonempty {X Y : Scheme.{u}} (f : X ⟶ Y) {n m : ℕ}
    (hn : SmoothOfRelativeDimension n f) (hm : SmoothOfRelativeDimension m f) [hX : Nonempty X] : n
      = m
theorem

exists_smoothOpen

L163 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.SmoothRestrictedPullbackDescent.AlgebraicGeometry.FibreCritPt.exists_smoothOpen
Source context 12 commands

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

section ProofImplementation
open _root_.AlgebraicGeometry.Scheme.Hom (
  fiberInclusion_mem_smoothLocus_of_mem_smoothLocus_fiberToSpecResidueField)
namespace AlgebraicCurves.Geometry.Schemes.Proofs.SmoothRestrictedPullbackDescent
attribute [-instance] TwoChartCech.Sections.M0_moduleA TwoChartCech.Sections.M1_module
  TwoChartCech.Cover.A01_algebra TwoChartCech.Cover.A0_algebra TwoChartCech.Cover.A1_commRing
  TwoChartCech.Cover.A1_algebra TwoChartCech.Sections.M01_module
  TwoChartCech.Sections.M0_addCommGroup TwoChartCech.Sections.M0_tower
  TwoChartCech.Sections.M01_addCommGroup TwoChartCech.Cover.A0_commRing
  TwoChartCech.Sections.M1_tower TwoChartCech.Sections.M01_moduleA TwoChartCech.Sections.M0_module
  TwoChartCech.Sections.M1_moduleA TwoChartCech.Sections.M1_addCommGroup
  TwoChartCech.Cover.A01_commRing TwoChartCech.Sections.M01_tower
  CoherentBaseChange.TwoTermComplex.C0_module CoherentBaseChange.TwoTermComplex.C0_addCommGroup
  CoherentBaseChange.TwoTermComplex.C1_module CoherentBaseChange.TwoTermComplex.C1_addCommGroup
  CoherentBaseChange.TwoTermComplex.C0_free CoherentBaseChange.TwoTermComplex.C1_finite
  CoherentBaseChange.TwoTermComplex.C0_finite CoherentBaseChange.TwoTermComplex.C1_free
attribute [-simp] AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.injEq
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U1
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U0 TwoChartCech.Sections.mk.injEq
  TwoChartCech.Cover.mk.injEq TwoChartCech.GrothendieckComplex.mk.injEq
  TwoChartCech.Sections.mk.sizeOf_spec TwoChartCech.Cover.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r0_apply TwoChartCech.GrothendieckComplex.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r1_apply CoherentBaseChange.TwoTermComplex.mk.sizeOf_spec
  CoherentBaseChange.TwoTermComplex.mk.injEq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
namespace FibreCritPt
open _root_.AlgebraicGeometry
Lean source · statement
theorem exists_smoothOpen
    {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
    [Flat c] [LocallyOfFinitePresentation c]
    {k : Type u} [Field k] (x : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of R))
    (Ω : (pullback c x).Opens) (hΩ : SmoothOfRelativeDimension 1 (Ω.ι ≫ pullback.snd c x)) :
    ∀ y ∈ (pullback.fst c x).base '' (Ω : Set ↥(pullback c x)),
      ∃ W : C.Opens, y ∈ W ∧ SmoothOfRelativeDimension 1 (W.ι ≫ c)
theorem

exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_opensRestrict_pullback_snd

L274 ↗
AlgebraicGeometry.exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_opensRestrict_pullback_snd
Source context 8 commands

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

section ProofImplementation
open _root_.AlgebraicGeometry.Scheme.Hom (
  fiberInclusion_mem_smoothLocus_of_mem_smoothLocus_fiberToSpecResidueField)
namespace AlgebraicGeometry
open _root_.AlgebraicCurves.Geometry.Schemes.Proofs.SmoothRestrictedPullbackDescent
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
Lean source · statement
theorem
exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_opensRestrict_pullback_snd
    {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
    [Flat c] [LocallyOfFinitePresentation c]
    {k : Type u} [Field k] (x : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of R))
    (Ω : (pullback c x).Opens) (hΩ : SmoothOfRelativeDimension 1 (Ω.ι ≫ pullback.snd c x)) :
    ∀ y ∈ (pullback.fst c x).base '' (Ω : Set ↥(pullback c x)),
      ∃ W : C.Opens, y ∈ W ∧ SmoothOfRelativeDimension 1 (W.ι ≫ c)

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