Module

SeparatedIntersections.lean

Nyll.SchemeTheory.Affine.SeparatedIntersections

5 declarations indexed from sourceView source ↗

Module documentation

Is Separated is Affine Open inf and exists eq sum mul of is Affine Open

Imports5

Mathlib.AlgebraicGeometry.Morphisms.Separated
Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Mathlib.AlgebraicGeometry.Pullbacks
Mathlib.LinearAlgebra.TensorProduct.Finiteness
Mathlib.Data.Fintype.EquivFin

Imported by4

theorem

opHom_eq

L34 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.IsSeparated_isAffineOpen_inf_and_exists_eq_sum_mul_of_isAffineOpen.IntSurj28.opHom_eq

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace IsSeparated_isAffineOpen_inf_and_exists_eq_sum_mul_of_isAffineOpen
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TensorProduct
namespace IntSurj28

Lean source · statement

theorem opHom_eq {X : Scheme.{u}} {A B : X.Opens} (i j : op A ⟶ op B) : i = j

theorem

topIso_hom_homOfLE_appTop

L37 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.IsSeparated_isAffineOpen_inf_and_exists_eq_sum_mul_of_isAffineOpen.IntSurj28.topIso_hom_homOfLE_appTop

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace IsSeparated_isAffineOpen_inf_and_exists_eq_sum_mul_of_isAffineOpen
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TensorProduct
namespace IntSurj28

Lean source · statement

theorem topIso_hom_homOfLE_appTop {X : Scheme.{u}} {U W : X.Opens} (e : W ≤ U) (a : Γ(X, U)) :
    W.topIso.hom ((X.homOfLE e).appTop (U.topIso.inv a)) = X.presheaf.map (homOfLE e).op a

theorem

exists_eq_specMap

L57 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.IsSeparated_isAffineOpen_inf_and_exists_eq_sum_mul_of_isAffineOpen.IntSurj28.exists_eq_specMap

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace IsSeparated_isAffineOpen_inf_and_exists_eq_sum_mul_of_isAffineOpen
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TensorProduct
namespace IntSurj28

Lean source · statement

theorem exists_eq_specMap {A R : CommRingCat.{u}} (g : Spec A ⟶ Spec R) :
    ∃ θ : R ⟶ A, Spec.map θ = g

theorem

main

L67 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.IsSeparated_isAffineOpen_inf_and_exists_eq_sum_mul_of_isAffineOpen.IntSurj28.main

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace IsSeparated_isAffineOpen_inf_and_exists_eq_sum_mul_of_isAffineOpen
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TensorProduct
namespace IntSurj28
section Main

Lean source · statement

theorem main {X Y : Scheme.{u}} (f : X ⟶ Y) [IsSeparated f] [IsAffine Y]
    (U V : X.Opens) (hU : IsAffineOpen U) (hV : IsAffineOpen V) :
    IsAffineOpen (U ⊓ V) ∧
    ∀ c : Γ(X, U ⊓ V), ∃ (n : ℕ) (a : Fin n → Γ(X, U)) (b : Fin n → Γ(X, V)),
      c = ∑ i : Fin n, X.presheaf.map (homOfLE inf_le_left).op (a i) *
        X.presheaf.map (homOfLE inf_le_right).op (b i)

theorem

isAffineOpen_inf_and_exists_eq_sum_mul_of_isAffineOpen

L177 ↗

AlgebraicGeometry.IsSeparated.isAffineOpen_inf_and_exists_eq_sum_mul_of_isAffineOpen

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace IsSeparated_isAffineOpen_inf_and_exists_eq_sum_mul_of_isAffineOpen
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TensorProduct

Lean source · statement

theorem _root_.AlgebraicGeometry.IsSeparated.isAffineOpen_inf_and_exists_eq_sum_mul_of_isAffineOpen
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsSeparated f] [IsAffine Y]
    (U V : X.Opens) (hU : IsAffineOpen U) (hV : IsAffineOpen V) :
    IsAffineOpen (U ⊓ V) ∧
    ∀ c : Γ(X, U ⊓ V), ∃ (n : ℕ) (a : Fin n → Γ(X, U)) (b : Fin n → Γ(X, V)),
      c = ∑ i : Fin n, X.presheaf.map (homOfLE inf_le_left).op (a i) * X.presheaf.map (homOfLE
        inf_le_right).op (b i)

Module documentation

Is Separated is Affine Open inf and exists eq sum mul of is Affine Open

Declarations

opHom_eq

topIso_hom_homOfLE_appTop

exists_eq_specMap

main

isAffineOpen_inf_and_exists_eq_sum_mul_of_isAffineOpen