Module

CurveModel_finite_integralClosure_sections_of_isIso_stalkMap.lean

Nyll.AlgebraicCurves.Models.CurveModel_finite_integralClosure_sections_of_isIso_stalkMap

1 declaration indexed from sourceView source ↗

Module documentation

Curve Model finite integral Closure sections of is Iso stalk Map

Imports8

Imported by2

theorem

finite_integralClosure_sections_of_isIso_stalkMap

L37 ↗

AlgebraicCurve.CurveModel.finite_integralClosure_sections_of_isIso_stalkMap

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_finite_integralClosure_sections_of_isIso_stalkMap
open _root_.AlgebraicCurve.CurveModel
universe u v
open CategoryTheory AlgebraicGeometry AlgebraicCurve
noncomputable section

Lean source · statement

theorem _root_.AlgebraicCurve.CurveModel.finite_integralClosure_sections_of_isIso_stalkMap
    (k : Type u) [Field k] [IsAlgClosed k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k))
      [IsIntegral C] [IsProper c]
    {F : Type v} [Field F] [Algebra k F] (M : AlgebraicCurve.CurveModel k F)
    (ν : M.C ⟶ C) (hν : ν ≫ c = M.toBase)
    (hbir : IsIso (ν.stalkMap (genericPoint M.C)))
    (U : C.Opens) (hUaff : IsAffineOpen U) [Nonempty U] :
    Module.Finite Γ(C, U) ↥(integralClosure Γ(C, U) C.functionField)

Module documentation

Curve Model finite integral Closure sections of is Iso stalk Map

Declarations

finite_integralClosure_sections_of_isIso_stalkMap