Module

Scheme_Hom_bijective_app_of_isPullback_of_bijective_of_isAffineOpen.lean

Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_Hom_bijective_app_of_isPullback_of_bijective_of_isAffineOpen

3 declarations indexed from sourceView source ↗

Module documentation

Scheme Hom bijective app of is Pullback of bijective of is Affine Open

Imports5

Mathlib.AlgebraicGeometry.Morphisms.Separated
Mathlib.AlgebraicGeometry.Morphisms.Flat
Mathlib.CategoryTheory.ConcreteCategory.EpiMono
Nyll.SchemeTheory.Cohomology.Cech.OrderedAffineCoverCech
Nyll.AlgebraicCurves.Geometry.Schemes.OrderedAffineCoverComap

Imported by2

theorem

flat_of_field

L34 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Hom_bijective_app_of_isPullback_of_bijective_of_isAffineOpen.C2KunnethH0Aux.flat_of_field

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_Hom_bijective_app_of_isPullback_of_bijective_of_isAffineOpen
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace C2KunnethH0Aux

Lean source · statement

theorem flat_of_field {k : Type u} [Field k] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of k)) :
    Flat f

theorem

bijective_appLE_top_iff

L40 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Hom_bijective_app_of_isPullback_of_bijective_of_isAffineOpen.C2KunnethH0Aux.bijective_appLE_top_iff

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_Hom_bijective_app_of_isPullback_of_bijective_of_isAffineOpen
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace C2KunnethH0Aux

Lean source · statement

theorem bijective_appLE_top_iff {X Y : Scheme.{u}} (f : X ⟶ Y) (e : (⊤ : X.Opens) ≤ f ⁻¹ᵁ ⊤) :
    Function.Bijective (f.appLE ⊤ ⊤ e).hom ↔ Function.Bijective f.appTop.hom

theorem

bijective_app_of_isPullback_of_bijective_of_isAffineOpen

L49 ↗

AlgebraicGeometry.Scheme.Hom.bijective_app_of_isPullback_of_bijective_of_isAffineOpen

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_Hom_bijective_app_of_isPullback_of_bijective_of_isAffineOpen
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
open C2KunnethH0Aux in

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.Hom.bijective_app_of_isPullback_of_bijective_of_isAffineOpen
    {k : Type u} [Field k] {X Y P : Scheme.{u}}
    (fX : X ⟶ Spec (CommRingCat.of k)) (fY : Y ⟶ Spec (CommRingCat.of k))
    [QuasiCompact fY] [IsSeparated fY]
    (hY : Function.Bijective ((Scheme.ΓSpecIso (CommRingCat.of k)).inv ≫ fY.appTop).hom)
    (p₁ : P ⟶ X) (p₂ : P ⟶ Y) (hP : IsPullback p₁ p₂ fX fY)
    (U : X.Opens) (hU : IsAffineOpen U) :
    Function.Bijective (p₁.app U).hom

Module documentation

Scheme Hom bijective app of is Pullback of bijective of is Affine Open

Declarations

flat_of_field

bijective_appLE_top_iff

bijective_app_of_isPullback_of_bijective_of_isAffineOpen