Module

geometricallyIntegral_of_bijective_algebraMap_sections_of_smooth.lean

Nyll.AlgebraicCurves.Geometry.Curves.geometricallyIntegral_of_bijective_algebraMap_sections_of_smooth

4 declarations indexed from sourceView source ↗

Module documentation

geometrically Integral of bijective algebra Map sections of smooth

Imports11

Mathlib.Algebra.Category.Ring.Constructions
Mathlib.Algebra.GroupWithZero.Idempotent
Mathlib.AlgebraicGeometry.Geometrically.Basic
Mathlib.AlgebraicGeometry.Geometrically.Integral
Mathlib.AlgebraicGeometry.Morphisms.Smooth
Mathlib.Topology.Connected.Clopen
Mathlib.Topology.Sheaves.CommRingCat
Mathlib.Topology.Sheaves.SheafCondition.Sites
Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
Nyll.SchemeTheory.Cohomology.Cech.TwoAffineOpenCover
Nyll.AlgebraicCurves.Geometry.Schemes.isIntegral_of_smooth_of_preconnectedSpace

Imported by1

Nyll.AlgebraicCurves.Geometry.Curves.All

theorem

connectedSpace_of_forall_isIdempotentElem

L56 ↗

AlgebraicCurves.Geometry.Curves.Proofs.geometricallyIntegral_of_bijective_algebraMap_sections_of_smooth.AlgebraicGeometry.Ws35Q1.connectedSpace_of_forall_isIdempotentElem

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace geometricallyIntegral_of_bijective_algebraMap_sections_of_smooth
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
namespace Ws35Q1
open _root_.AlgebraicGeometry

Lean source · statement

theorem connectedSpace_of_forall_isIdempotentElem {X : Scheme.{u}} [Nontrivial Γ(X, ⊤)]
    (h : ∀ e : Γ(X, ⊤), IsIdempotentElem e → e = 0 ∨ e = 1) : ConnectedSpace X

theorem

connectedSpace_of_bijective

L121 ↗

AlgebraicCurves.Geometry.Curves.Proofs.geometricallyIntegral_of_bijective_algebraMap_sections_of_smooth.AlgebraicGeometry.Ws35Q1.connectedSpace_of_bijective

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace geometricallyIntegral_of_bijective_algebraMap_sections_of_smooth
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
namespace Ws35Q1
open _root_.AlgebraicGeometry

Lean source · statement

theorem connectedSpace_of_bijective {K : Type u} [Field K] {X : Scheme.{u}} (φ : K →+* Γ(X, ⊤))
    (hφ : Function.Bijective φ) : ConnectedSpace X

instance

isClosedUnderIsomorphisms_isIntegral

L133 ↗

AlgebraicCurves.Geometry.Curves.Proofs.geometricallyIntegral_of_bijective_algebraMap_sections_of_smooth.AlgebraicGeometry.Ws35Q1.isClosedUnderIsomorphisms_isIntegral

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace geometricallyIntegral_of_bijective_algebraMap_sections_of_smooth
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
namespace Ws35Q1
open _root_.AlgebraicGeometry

Lean source · full declaration

instance isClosedUnderIsomorphisms_isIntegral :
    ObjectProperty.IsClosedUnderIsomorphisms (C := Scheme.{u}) (fun X : Scheme.{u} => IsIntegral X)
      :=
  ⟨fun e h => by have := h; exact IsIntegral.of_isIso e.hom⟩

theorem

geometricallyIntegral_of_bijective_algebraMap_sections_of_smooth

L148 ↗

AlgebraicGeometry.geometricallyIntegral_of_bijective_algebraMap_sections_of_smooth

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace geometricallyIntegral_of_bijective_algebraMap_sections_of_smooth
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
attribute [local instance]
  AlgebraicGeometry.Ws35Q1.isClosedUnderIsomorphisms_isIntegral
open AlgebraicGeometry.Ws35Q1 in

Lean source · full declaration

theorem _root_.AlgebraicGeometry.geometricallyIntegral_of_bijective_algebraMap_sections_of_smooth
    {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R)) [Smooth c]
    (hH0 : ∀ (A : Type u) [CommRing A] [Algebra R A],
      letI := Scheme.TwoAffineOpenCover.algebraOfHom
        (Limits.pullback.snd c (Scheme.TwoAffineOpenCover.specMap R A)) ⊤
      Function.Bijective (algebraMap A Γ(Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R A),
        ⊤))) :
    GeometricallyIntegral c := by
  refine ⟨(geometrically_iff_of_commRing_of_isClosedUnderIsomorphisms (P := fun X : Scheme.{u} =>
    IsIntegral X)).mpr ?_⟩
  intro K _ _
  let := Scheme.TwoAffineOpenCover.algebraOfHom
    (Limits.pullback.snd c (Scheme.TwoAffineOpenCover.specMap R K)) ⊤
  have : ConnectedSpace ↥(Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R K)) :=
    connectedSpace_of_bijective (algebraMap K _) (hH0 K)
  exact AlgebraicGeometry.isIntegral_of_smooth_of_preconnectedSpace
    (Limits.pullback.snd c (Scheme.TwoAffineOpenCover.specMap R K))

Module documentation

geometrically Integral of bijective algebra Map sections of smooth

Declarations

connectedSpace_of_forall_isIdempotentElem

connectedSpace_of_bijective

isClosedUnderIsomorphisms_isIntegral

geometricallyIntegral_of_bijective_algebraMap_sections_of_smooth