Module

AbelianSchemePropertyBundle_geometricallyIntegral.lean

Nyll.AlgebraicCurves.Geometry.AbelianSchemes.Theorems.AbelianSchemePropertyBundle_geometricallyIntegral

10 declarations indexed from sourceView source ↗

Module documentation

Abelian Scheme Property Bundle geometrically Integral

Imports7

Imported by10

theorem

isIntegral_of_smooth_of_connectedSpace

L36 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.AbelianSchemePropertyBundle_geometricallyIntegral.S17A0.isIntegral_of_smooth_of_connectedSpace

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace AbelianSchemePropertyBundle_geometricallyIntegral
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
namespace S17A0

Lean source · statement

theorem isIntegral_of_smooth_of_connectedSpace {K : Type u} [Field K] {X : Scheme.{u}}
    (t : X ⟶ Spec (CommRingCat.of K)) [Smooth t] [ConnectedSpace X] : IsIntegral X

instance

subsingleton_spec_field

L46 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.AbelianSchemePropertyBundle_geometricallyIntegral.S17A0.subsingleton_spec_field

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace AbelianSchemePropertyBundle_geometricallyIntegral
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
namespace S17A0

Lean source · statement

instance subsingleton_spec_field (K : Type u) [Field K] :
    Subsingleton ↥(Spec (CommRingCat.of K))

instance

nonempty_spec_field

L50 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.AbelianSchemePropertyBundle_geometricallyIntegral.S17A0.nonempty_spec_field

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace AbelianSchemePropertyBundle_geometricallyIntegral
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
namespace S17A0

Lean source · statement

instance nonempty_spec_field (K : Type u) [Field K] :
    Nonempty ↥(Spec (CommRingCat.of K))

abbrev

bc

L61 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.AbelianSchemePropertyBundle_geometricallyIntegral.S17A0.bc

Documentation

The morphism of spectra induced by the algebra map from the base field to its extension.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace AbelianSchemePropertyBundle_geometricallyIntegral
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
namespace S17A0
section Stacks04KV
variable {k K : Type u} [Field k] [Field K] [Algebra k K]
  {A : Scheme.{u}} (f : A ⟶ Spec (CommRingCat.of k))
  (e : Spec (CommRingCat.of k) ⟶ A) (he : e ≫ f = 𝟙 _)

Lean source · statement

abbrev bc (k K : Type u) [Field k] [Field K] [Algebra k K] :
    Spec (CommRingCat.of K) ⟶ Spec (CommRingCat.of k)

def

pt'

L67 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.AbelianSchemePropertyBundle_geometricallyIntegral.S17A0.pt'

Documentation

The section after base change to K, obtained by lifting the original section through the pullback.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace AbelianSchemePropertyBundle_geometricallyIntegral
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
namespace S17A0
section Stacks04KV
variable {k K : Type u} [Field k] [Field K] [Algebra k K]
  {A : Scheme.{u}} (f : A ⟶ Spec (CommRingCat.of k))
  (e : Spec (CommRingCat.of k) ⟶ A) (he : e ≫ f = 𝟙 _)

Lean source · statement

def pt' : Spec (CommRingCat.of K) ⟶ pullback f (bc k K)

theorem

pt'_fst

L70 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.AbelianSchemePropertyBundle_geometricallyIntegral.S17A0.pt'_fst

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace AbelianSchemePropertyBundle_geometricallyIntegral
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
namespace S17A0
section Stacks04KV
variable {k K : Type u} [Field k] [Field K] [Algebra k K]
  {A : Scheme.{u}} (f : A ⟶ Spec (CommRingCat.of k))
  (e : Spec (CommRingCat.of k) ⟶ A) (he : e ≫ f = 𝟙 _)

Lean source · statement

theorem pt'_fst : pt' f e he ≫ pullback.fst f (bc k K) = bc k K ≫ e

theorem

subsingleton_pullback_section

L73 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.AbelianSchemePropertyBundle_geometricallyIntegral.S17A0.subsingleton_pullback_section

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace AbelianSchemePropertyBundle_geometricallyIntegral
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
namespace S17A0
section Stacks04KV
variable {k K : Type u} [Field k] [Field K] [Algebra k K]
  {A : Scheme.{u}} (f : A ⟶ Spec (CommRingCat.of k))
  (e : Spec (CommRingCat.of k) ⟶ A) (he : e ≫ f = 𝟙 _)
include he in

Lean source · statement

theorem subsingleton_pullback_section :
    Subsingleton ↥(pullback e (pullback.fst f (bc k K)))

theorem

eq_pt'_of_fst_eq

L84 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.AbelianSchemePropertyBundle_geometricallyIntegral.S17A0.eq_pt'_of_fst_eq

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace AbelianSchemePropertyBundle_geometricallyIntegral
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
namespace S17A0
section Stacks04KV
variable {k K : Type u} [Field k] [Field K] [Algebra k K]
  {A : Scheme.{u}} (f : A ⟶ Spec (CommRingCat.of k))
  (e : Spec (CommRingCat.of k) ⟶ A) (he : e ≫ f = 𝟙 _)

Lean source · statement

theorem eq_pt'_of_fst_eq (v : ↥(pullback f (bc k K)))
    (hv : pullback.fst f (bc k K) v = e (IsLocalRing.closedPoint k)) :
    v = pt' f e he (IsLocalRing.closedPoint K)

theorem

connectedSpace_pullback

L103 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.AbelianSchemePropertyBundle_geometricallyIntegral.S17A0.connectedSpace_pullback

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace AbelianSchemePropertyBundle_geometricallyIntegral
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
namespace S17A0
section Stacks04KV
variable {k K : Type u} [Field k] [Field K] [Algebra k K]
  {A : Scheme.{u}} (f : A ⟶ Spec (CommRingCat.of k))
  (e : Spec (CommRingCat.of k) ⟶ A) (he : e ≫ f = 𝟙 _)
include he in

Lean source · statement

theorem connectedSpace_pullback [Algebra.IsAlgebraic k K] [ConnectedSpace A] :
    ConnectedSpace ↥(pullback f (bc k K))

theorem

geometricallyIntegral

L142 ↗

GoodReductionJacobian.AbelianSchemePropertyBundle.geometricallyIntegral

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace AbelianSchemePropertyBundle_geometricallyIntegral
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
open S17A0 in

Lean source · statement

theorem _root_.GoodReductionJacobian.AbelianSchemePropertyBundle.geometricallyIntegral
    {k : Type u} [Field k] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of k)}
    (hA : AbelianSchemePropertyBundle k f) : GeometricallyIntegral f

Module documentation

Abelian Scheme Property Bundle geometrically Integral

Declarations