Module

geometricallyConnected_of_bijective_algebraMap_sections.lean

Nyll.AlgebraicCurves.Geometry.Curves.geometricallyConnected_of_bijective_algebraMap_sections

4 declarations indexed from sourceView source ↗

Module documentation

geometrically Connected of bijective algebra Map sections

Imports5

Mathlib.AlgebraicGeometry.Geometrically.Connected
Mathlib.Topology.Sheaves.CommRingCat
Mathlib.Algebra.GroupWithZero.Idempotent
Batteries.Tactic.Init
Nyll.SchemeTheory.Cohomology.Cech.TwoAffineOpenCover

Imported by2

theorem

connectedSpace_of_forall_isIdempotentElem

L50 ↗

AlgebraicCurves.Geometry.Curves.Proofs.geometricallyConnected_of_bijective_algebraMap_sections.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 geometricallyConnected_of_bijective_algebraMap_sections
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

L115 ↗

AlgebraicCurves.Geometry.Curves.Proofs.geometricallyConnected_of_bijective_algebraMap_sections.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 geometricallyConnected_of_bijective_algebraMap_sections
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

L127 ↗

AlgebraicCurves.Geometry.Curves.Proofs.geometricallyConnected_of_bijective_algebraMap_sections.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 geometricallyConnected_of_bijective_algebraMap_sections
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

geometricallyConnected_of_bijective_algebraMap_sections

L139 ↗

AlgebraicGeometry.geometricallyConnected_of_bijective_algebraMap_sections

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace geometricallyConnected_of_bijective_algebraMap_sections
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.geometricallyConnected_of_bijective_algebraMap_sections
    {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
    (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),
        ⊤))) :
    GeometricallyConnected c := by
  refine ⟨(geometrically_iff_of_commRing_of_isClosedUnderIsomorphisms (P := (ConnectedSpace
    ·))).mpr ?_⟩
  intro K _ _
  let := Scheme.TwoAffineOpenCover.algebraOfHom
    (Limits.pullback.snd c (Scheme.TwoAffineOpenCover.specMap R K)) ⊤
  exact connectedSpace_of_bijective (algebraMap K Γ(Limits.pullback c
    (Scheme.TwoAffineOpenCover.specMap R K), ⊤)) (hH0 K)

Module documentation

geometrically Connected of bijective algebra Map sections

Declarations

connectedSpace_of_forall_isIdempotentElem

connectedSpace_of_bijective

isClosedUnderIsomorphisms_isIntegral

geometricallyConnected_of_bijective_algebraMap_sections