Module

CurveModel_exists_eq_appTop_of_isUnit.lean

Nyll.AlgebraicCurves.Models.CurveModel_exists_eq_appTop_of_isUnit

1 declaration indexed from sourceView source ↗

Module documentation

Curve Model exists eq app Top of is Unit

Imports2

Nyll.AlgebraicCurves.Models.Basic
Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero

Imported by1

Nyll.AlgebraicCurves.Models.All

theorem

exists_eq_appTop_of_isUnit

L28 ↗

AlgebraicCurve.CurveModel.exists_eq_appTop_of_isUnit

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_eq_appTop_of_isUnit
universe u
open CategoryTheory AlgebraicGeometry AlgebraicCurve

Lean source · statement

theorem _root_.AlgebraicCurve.CurveModel.exists_eq_appTop_of_isUnit
    (k : Type u) [Field k] [IsAlgClosed k] (M : CurveModel k (RatFunc k))
    (u : Γ(M.C, ⊤)) (hu : IsUnit u) :
    ∃ c : k, u = M.toBase.appTop ((Scheme.ΓSpecIso (CommRingCat.of k)).inv c)

Module documentation

Curve Model exists eq app Top of is Unit

Declarations

exists_eq_appTop_of_isUnit