Module

Scheme_existsUnique_section_algebraMap_germ_eq_of_forall_mem_range.lean

Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_existsUnique_section_algebraMap_germ_eq_of_forall_mem_range

7 declarations indexed from sourceView source ↗

Module documentation

Scheme exists Unique section algebra Map germ eq of forall mem range

Imports20

Mathlib.Algebra.Algebra.Defs
Mathlib.Algebra.Category.Ring.Basic
Mathlib.Algebra.Category.Ring.FilteredColimits
Mathlib.Algebra.Category.Ring.Limits
Mathlib.Algebra.Group.Hom.Defs
Mathlib.Algebra.Group.Monoid
Mathlib.Algebra.Group.Units.Defs
Mathlib.Algebra.GroupWithZero.Defs
Mathlib.Algebra.Ring.Subring.Basic
Mathlib.AlgebraicGeometry.FunctionField
Mathlib.AlgebraicGeometry.Properties
Mathlib.AlgebraicGeometry.Scheme
Mathlib.CategoryTheory.Category.Preorder
Mathlib.Tactic.Choose
Mathlib.Tactic.Push
Mathlib.Topology.Inseparable
Mathlib.Topology.Sets.Opens
Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
Mathlib.Topology.Sheaves.Stalks
Mathlib.Topology.Sober

Imported by2

theorem

algebraMap_germ

L51 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_existsUnique_section_algebraMap_germ_eq_of_forall_mem_range.KLiftAux.algebraMap_germ

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_existsUnique_section_algebraMap_germ_eq_of_forall_mem_range
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace KLiftAux
variable {X : Scheme.{u}} [IsIntegral X]

Lean source · statement

theorem algebraMap_germ (W : X.Opens) (t : Γ(X, W)) (x : X) (hx : x ∈ W) :
    algebraMap (X.presheaf.stalk x) X.functionField (X.presheaf.germ W x hx t) =
      X.presheaf.germ W (genericPoint X)
        (((genericPoint_spec X).specializes (Set.mem_univ x)).mem_open W.isOpen hx) t

theorem

algebraMap_germ_eq

L59 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_existsUnique_section_algebraMap_germ_eq_of_forall_mem_range.KLiftAux.algebraMap_germ_eq

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_existsUnique_section_algebraMap_germ_eq_of_forall_mem_range
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace KLiftAux
variable {X : Scheme.{u}} [IsIntegral X]

Lean source · statement

theorem algebraMap_germ_eq (W : X.Opens) (t : Γ(X, W)) (x y : X) (hx : x ∈ W) (hy : y ∈ W) :
    algebraMap (X.presheaf.stalk x) X.functionField (X.presheaf.germ W x hx t) =
      algebraMap (X.presheaf.stalk y) X.functionField (X.presheaf.germ W y hy t)

theorem

section_eq_of_algebraMap_germ_eq

L64 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_existsUnique_section_algebraMap_germ_eq_of_forall_mem_range.KLiftAux.section_eq_of_algebraMap_germ_eq

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_existsUnique_section_algebraMap_germ_eq_of_forall_mem_range
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace KLiftAux
variable {X : Scheme.{u}} [IsIntegral X]

Lean source · statement

theorem section_eq_of_algebraMap_germ_eq (W : X.Opens) (t t' : Γ(X, W)) (x : X) (hx : x ∈ W)
    (h : algebraMap (X.presheaf.stalk x) X.functionField (X.presheaf.germ W x hx t) =
      algebraMap (X.presheaf.stalk x) X.functionField (X.presheaf.germ W x hx t')) : t = t'

theorem

section_eq_of_isEmpty

L72 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_existsUnique_section_algebraMap_germ_eq_of_forall_mem_range.KLiftAux.section_eq_of_isEmpty

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_existsUnique_section_algebraMap_germ_eq_of_forall_mem_range
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace KLiftAux
variable {X : Scheme.{u}} [IsIntegral X]
omit [IsIntegral X] in

Lean source · statement

theorem section_eq_of_isEmpty (W : X.Opens) (hW : ∀ x : X, x ∉ W) (t t' : Γ(X, W)) : t = t'

theorem

exists_section_algebraMap_germ_eq

L76 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_existsUnique_section_algebraMap_germ_eq_of_forall_mem_range.KLiftAux.exists_section_algebraMap_germ_eq

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_existsUnique_section_algebraMap_germ_eq_of_forall_mem_range
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace KLiftAux
variable {X : Scheme.{u}} [IsIntegral X]

Lean source · statement

theorem exists_section_algebraMap_germ_eq (W : X.Opens) (s : X.functionField)
    (hs : ∀ x ∈ W, s ∈ (algebraMap (X.presheaf.stalk x) X.functionField).range) :
    ∃ u : Γ(X, W), ∀ (x : X) (hx : x ∈ W),
      algebraMap (X.presheaf.stalk x) X.functionField (X.presheaf.germ W x hx u) = s

theorem

exists_unit_section_algebraMap_germ_eq

L121 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_existsUnique_section_algebraMap_germ_eq_of_forall_mem_range.KLiftAux.exists_unit_section_algebraMap_germ_eq

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_existsUnique_section_algebraMap_germ_eq_of_forall_mem_range
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace KLiftAux
variable {X : Scheme.{u}} [IsIntegral X]

Lean source · statement

theorem exists_unit_section_algebraMap_germ_eq (W : X.Opens) (s : X.functionField) (hs0 : s ≠ 0)
    (hs : ∀ x ∈ W, s ∈ (algebraMap (X.presheaf.stalk x) X.functionField).range)
    (hs' : ∀ x ∈ W, s⁻¹ ∈ (algebraMap (X.presheaf.stalk x) X.functionField).range) :
    ∃ u : Γ(X, W), (∀ (x : X) (hx : x ∈ W),
      algebraMap (X.presheaf.stalk x) X.functionField (X.presheaf.germ W x hx u) = s) ∧ IsUnit u

theorem

existsUnique_section_algebraMap_germ_eq_of_forall_mem_range

L141 ↗

AlgebraicGeometry.Scheme.existsUnique_section_algebraMap_germ_eq_of_forall_mem_range

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_existsUnique_section_algebraMap_germ_eq_of_forall_mem_range
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.existsUnique_section_algebraMap_germ_eq_of_forall_mem_range
    {X : Scheme.{u}} [IsIntegral X] (W : X.Opens) (s : X.functionField)
    (hs : ∀ x ∈ W, s ∈ (algebraMap (X.presheaf.stalk x) X.functionField).range) :
    ∃! u : Γ(X, W), ∀ (x : X) (hx : x ∈ W),
      algebraMap (X.presheaf.stalk x) X.functionField (X.presheaf.germ W x hx u) = s

Module documentation

Scheme exists Unique section algebra Map germ eq of forall mem range

Declarations

algebraMap_germ

algebraMap_germ_eq

section_eq_of_algebraMap_germ_eq

section_eq_of_isEmpty

exists_section_algebraMap_germ_eq

exists_unit_section_algebraMap_germ_eq

existsUnique_section_algebraMap_germ_eq_of_forall_mem_range