Module

IsAffineOpen_eq_of_appLE_eq_and_exists_appLE_eq_of_ringHom.lean

Nyll.AlgebraicCurves.Geometry.Schemes.IsAffineOpen_eq_of_appLE_eq_and_exists_appLE_eq_of_ringHom

3 declarations indexed from sourceView source ↗

Module documentation

Is Affine Open eq of app LE eq and exists app LE eq of ring Hom

Imports15

Mathlib.Algebra.Category.Ring.Basic
Mathlib.Algebra.Field.Defs
Mathlib.Algebra.Ring.Hom.Defs
Mathlib.AlgebraicGeometry.AffineScheme
Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Mathlib.AlgebraicGeometry.OpenImmersion
Mathlib.AlgebraicGeometry.Restrict
Mathlib.AlgebraicGeometry.Scheme
Mathlib.CategoryTheory.Category.Basic
Mathlib.CategoryTheory.Functor.Basic
Mathlib.CategoryTheory.Iso
Mathlib.Data.FunLike.Basic
Mathlib.Tactic.Conv
Mathlib.Tactic.Convert
Mathlib.Topology.Category.TopCat.Basic

Imported by3

theorem

Spec_hom_ext

L44 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.IsAffineOpen_eq_of_appLE_eq_and_exists_appLE_eq_of_ringHom.KPoints29.Spec_hom_ext

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace IsAffineOpen_eq_of_appLE_eq_and_exists_appLE_eq_of_ringHom
universe u
open CategoryTheory AlgebraicGeometry Opposite
namespace KPoints29

Lean source · statement

theorem Spec_hom_ext {R S : CommRingCat.{u}} {g h : Spec S ⟶ Spec R} (e : g.appTop = h.appTop) : g
  = h

theorem

appLE_of_fac

L55 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.IsAffineOpen_eq_of_appLE_eq_and_exists_appLE_eq_of_ringHom.KPoints29.appLE_of_fac

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace IsAffineOpen_eq_of_appLE_eq_and_exists_appLE_eq_of_ringHom
universe u
open CategoryTheory AlgebraicGeometry Opposite
namespace KPoints29
variable {K : Type u} [Field K] {X : Scheme.{u}} (W : X.Opens)

Lean source · statement

theorem appLE_of_fac (p : Spec (CommRingCat.of K) ⟶ X) (p' : Spec (CommRingCat.of K) ⟶ W) (hfac :
  p' ≫ W.ι = p)
    (hp : ⊤ ≤ p ⁻¹ᵁ W) :
    p.appLE W ⊤ hp = W.topIso.inv ≫ p'.appTop

theorem

eq_of_appLE_eq_and_exists_appLE_eq_of_ringHom

L70 ↗

AlgebraicGeometry.IsAffineOpen.eq_of_appLE_eq_and_exists_appLE_eq_of_ringHom

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace IsAffineOpen_eq_of_appLE_eq_and_exists_appLE_eq_of_ringHom
universe u
open CategoryTheory AlgebraicGeometry Opposite
open KPoints29

Lean source · statement

theorem _root_.AlgebraicGeometry.IsAffineOpen.eq_of_appLE_eq_and_exists_appLE_eq_of_ringHom
    {K : Type u} [Field K] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of K))
    (W : X.Opens) (hW : IsAffineOpen W) :
    (∀ (p q : Spec (CommRingCat.of K) ⟶ X), p ≫ f = 𝟙 _ → q ≫ f = 𝟙 _ →
      ∀ (hp : ⊤ ≤ p ⁻¹ᵁ W) (hq : ⊤ ≤ q ⁻¹ᵁ W),
        p.appLE W ⊤ hp ≫ (Scheme.ΓSpecIso (CommRingCat.of K)).hom =
          q.appLE W ⊤ hq ≫ (Scheme.ΓSpecIso (CommRingCat.of K)).hom → p = q) ∧
    (∀ ν : Γ(X, W) →+* K,
        ν.comp ((Scheme.ΓSpecIso (CommRingCat.of K)).inv ≫ f.appLE ⊤ W le_top).hom = RingHom.id K →
        ∃ (p : Spec (CommRingCat.of K) ⟶ X) (_ : p ≫ f = 𝟙 _) (hp : ⊤ ≤ p ⁻¹ᵁ W),
          (p.appLE W ⊤ hp ≫ (Scheme.ΓSpecIso (CommRingCat.of K)).hom).hom = ν)

Module documentation

Is Affine Open eq of app LE eq and exists app LE eq of ring Hom

Declarations

Spec_hom_ext

appLE_of_fac

eq_of_appLE_eq_and_exists_appLE_eq_of_ringHom