Module

AbelianSchemePropertyBundle_flat_of_isFinite.lean

Nyll.AlgebraicCurves.Geometry.AbelianSchemes.Theorems.AbelianSchemePropertyBundle_flat_of_isFinite

4 declarations indexed from sourceView source ↗

Module documentation

Abelian Scheme Property Bundle flat of is Finite

Imports7

Imported by4

theorem

isLocallyNoetherian

L41 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.AbelianSchemePropertyBundle_flat_of_isFinite.P2mIsogFlat.isLocallyNoetherian

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace AbelianSchemePropertyBundle_flat_of_isFinite
attribute [-simp] RegularLocalRingQuotientAscent.dualNumberFst_apply
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mIsogFlat
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}

Lean source · statement

theorem isLocallyNoetherian (hA : AbelianSchemePropertyBundle K f) : IsLocallyNoetherian A

theorem

flat_stalkMap

L47 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.AbelianSchemePropertyBundle_flat_of_isFinite.P2mIsogFlat.flat_stalkMap

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace AbelianSchemePropertyBundle_flat_of_isFinite
attribute [-simp] RegularLocalRingQuotientAscent.dualNumberFst_apply
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mIsogFlat
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}

Lean source · statement

theorem flat_stalkMap (hA : AbelianSchemePropertyBundle K f) (β : SchemeHomOver f f)
    [IsFinite β.1] (x : A) : (β.1.stalkMap x).hom.Flat

theorem

main

L71 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.AbelianSchemePropertyBundle_flat_of_isFinite.P2mIsogFlat.main

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace AbelianSchemePropertyBundle_flat_of_isFinite
attribute [-simp] RegularLocalRingQuotientAscent.dualNumberFst_apply
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mIsogFlat
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}

Lean source · statement

theorem main (hA : AbelianSchemePropertyBundle K f) (β : SchemeHomOver f f) [IsFinite β.1] :
    Flat β.1

theorem

flat_of_isFinite

L77 ↗

GoodReductionJacobian.AbelianSchemePropertyBundle.flat_of_isFinite

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace AbelianSchemePropertyBundle_flat_of_isFinite
attribute [-simp] RegularLocalRingQuotientAscent.dualNumberFst_apply
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u

Lean source · statement

theorem _root_.GoodReductionJacobian.AbelianSchemePropertyBundle.flat_of_isFinite
    (K : Type u) [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}
    (hA : AbelianSchemePropertyBundle K f) (β : SchemeHomOver f f) [IsFinite β.1] :
    Flat β.1

Module documentation

Abelian Scheme Property Bundle flat of is Finite

Declarations

isLocallyNoetherian

flat_stalkMap

main

flat_of_isFinite