Module

exists_comp_eq_of_isOpenImmersion_of_abelianSchemePropertyBundle.lean

Nyll.AlgebraicCurves.Geometry.Picard.exists_comp_eq_of_isOpenImmersion_of_abelianSchemePropertyBundle

6 declarations indexed from sourceView source ↗

Module documentation

exists comp eq of is Open Immersion of abelian Scheme Property Bundle

Imports9

Mathlib.AlgebraicGeometry.Birational.RationalMap
Mathlib.AlgebraicGeometry.ValuativeCriterion
Mathlib.AlgebraicGeometry.Morphisms.Smooth
Mathlib.RingTheory.DiscreteValuationRing.TFAE
Nyll.AlgebraicCurves.Geometry.AbelianSchemes.AbelianSchemePropertyBundle
Nyll.AlgebraicCurves.Geometry.AbelianSchemes.Theorems.RelativeGroupLaw_exists_opens_diagonal_difference_extension_of_forall_ringKrullDim_le_one
Nyll.AlgebraicCurves.Geometry.AbelianSchemes.Theorems.RelativeGroupLaw_exists_extension_of_diagonal_difference_extension_of_dense
Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_PartialMap_mem_domain_toRationalMap_of_valuationRing_stalk
Nyll.SchemeTheory.LocalGeometry.SmoothStalkNormality

Imported by3

instance

isDomain_sections_spec

L64 ↗

AlgebraicCurves.Geometry.Picard.Proofs.exists_comp_eq_of_isOpenImmersion_of_abelianSchemePropertyBundle.AlgebraicGeometry.WeilExtField.EXT.isDomain_sections_spec

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace exists_comp_eq_of_isOpenImmersion_of_abelianSchemePropertyBundle
attribute [-instance] instTopologicallyFGOfFiniteType
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
universe u
noncomputable section
namespace AlgebraicGeometry
namespace WeilExtField
namespace EXT
open _root_.AlgebraicGeometry

Lean source · statement

instance isDomain_sections_spec (k : Type u) [Field k] :
    IsDomain Γ(Spec (CommRingCat.of k), ⊤)

instance

isIntegrallyClosed_sections_spec

L68 ↗

AlgebraicCurves.Geometry.Picard.Proofs.exists_comp_eq_of_isOpenImmersion_of_abelianSchemePropertyBundle.AlgebraicGeometry.WeilExtField.EXT.isIntegrallyClosed_sections_spec

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace exists_comp_eq_of_isOpenImmersion_of_abelianSchemePropertyBundle
attribute [-instance] instTopologicallyFGOfFiniteType
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
universe u
noncomputable section
namespace AlgebraicGeometry
namespace WeilExtField
namespace EXT
open _root_.AlgebraicGeometry

Lean source · statement

instance isIntegrallyClosed_sections_spec (k : Type u) [Field k] :
    IsIntegrallyClosed Γ(Spec (CommRingCat.of k), ⊤)

theorem

isReduced_of_smooth

L72 ↗

AlgebraicCurves.Geometry.Picard.Proofs.exists_comp_eq_of_isOpenImmersion_of_abelianSchemePropertyBundle.AlgebraicGeometry.WeilExtField.EXT.isReduced_of_smooth

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace exists_comp_eq_of_isOpenImmersion_of_abelianSchemePropertyBundle
attribute [-instance] instTopologicallyFGOfFiniteType
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
universe u
noncomputable section
namespace AlgebraicGeometry
namespace WeilExtField
namespace EXT
open _root_.AlgebraicGeometry

Lean source · statement

theorem isReduced_of_smooth (k : Type u) [Field k] {X : Scheme.{u}}
    (g : X ⟶ Spec (CommRingCat.of k)) [Smooth g] : IsReduced X

theorem

valuationRing_stalk_of_ringKrullDim_le_one

L79 ↗

AlgebraicCurves.Geometry.Picard.Proofs.exists_comp_eq_of_isOpenImmersion_of_abelianSchemePropertyBundle.AlgebraicGeometry.WeilExtField.EXT.valuationRing_stalk_of_ringKrullDim_le_one

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace exists_comp_eq_of_isOpenImmersion_of_abelianSchemePropertyBundle
attribute [-instance] instTopologicallyFGOfFiniteType
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
universe u
noncomputable section
namespace AlgebraicGeometry
namespace WeilExtField
namespace EXT
open _root_.AlgebraicGeometry

Lean source · statement

theorem valuationRing_stalk_of_ringKrullDim_le_one (k : Type u) [Field k] {X : Scheme.{u}}
  [IsIntegral X]
    (g : X ⟶ Spec (CommRingCat.of k)) [Smooth g] (x : X)
    (hx : ringKrullDim (X.presheaf.stalk x) ≤ 1) : ValuationRing (X.presheaf.stalk x)

theorem

main

L91 ↗

AlgebraicCurves.Geometry.Picard.Proofs.exists_comp_eq_of_isOpenImmersion_of_abelianSchemePropertyBundle.AlgebraicGeometry.WeilExtField.EXT.main

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace exists_comp_eq_of_isOpenImmersion_of_abelianSchemePropertyBundle
attribute [-instance] instTopologicallyFGOfFiniteType
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
universe u
noncomputable section
namespace AlgebraicGeometry
namespace WeilExtField
namespace EXT
open _root_.AlgebraicGeometry
open _root_.GoodReductionJacobian.RelativeGroupLaw in

Lean source · statement

theorem main
    {k : Type u} [Field k] {X : Scheme.{u}} (g : X ⟶ Spec (CommRingCat.of k))
    [Smooth g] [IsSeparated g] [QuasiCompact g] [IrreducibleSpace X]
    {A : Scheme.{u}} {fA : A ⟶ Spec (CommRingCat.of k)} (hA : AbelianSchemePropertyBundle k fA)
    {U : Scheme.{u}} (u : U ⟶ X) [IsOpenImmersion u] [Nonempty U]
    (φ : U ⟶ A) (hφ : φ ≫ fA = u ≫ g) :
    ∃ ψ : X ⟶ A, ψ ≫ fA = g ∧ u ≫ ψ = φ

theorem

exists_comp_eq_of_isOpenImmersion_of_abelianSchemePropertyBundle

L179 ↗

AlgebraicGeometry.exists_comp_eq_of_isOpenImmersion_of_abelianSchemePropertyBundle

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace exists_comp_eq_of_isOpenImmersion_of_abelianSchemePropertyBundle
attribute [-instance] instTopologicallyFGOfFiniteType
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
universe u
attribute [local instance]
  AlgebraicGeometry.WeilExtField.EXT.isDomain_sections_spec
attribute [local instance]
  AlgebraicGeometry.WeilExtField.EXT.isIntegrallyClosed_sections_spec

Lean source · statement

theorem _root_.AlgebraicGeometry.exists_comp_eq_of_isOpenImmersion_of_abelianSchemePropertyBundle
    {k : Type u} [Field k] {X : Scheme.{u}} (g : X ⟶ Spec (CommRingCat.of k))
    [Smooth g] [IsSeparated g] [QuasiCompact g] [IrreducibleSpace X]
    {A : Scheme.{u}} {fA : A ⟶ Spec (CommRingCat.of k)} (hA : AbelianSchemePropertyBundle k fA)
    {U : Scheme.{u}} (u : U ⟶ X) [IsOpenImmersion u] [Nonempty U]
    (φ : U ⟶ A) (hφ : φ ≫ fA = u ≫ g) :
    ∃ ψ : X ⟶ A, ψ ≫ fA = g ∧ u ≫ ψ = φ

Module documentation

exists comp eq of is Open Immersion of abelian Scheme Property Bundle

Declarations

isDomain_sections_spec

isIntegrallyClosed_sections_spec

isReduced_of_smooth

valuationRing_stalk_of_ringKrullDim_le_one

main

exists_comp_eq_of_isOpenImmersion_of_abelianSchemePropertyBundle