NYLL
Module

Scheme_TwoAffineOpenCover_nonempty_iso_iff_exists_units_of_sectionsOf_equiv_lineBundle.lean

Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_TwoAffineOpenCover_nonempty_iso_iff_exists_units_of_sectionsOf_equiv_lineBundle
8 declarations indexed from sourceView source ↗

Module documentation

Scheme Two Affine Open Cover nonempty iso iff exists units of sections Of equiv line

Bundle

Imports4
Imported by2

Declarations

theorem

linearEquiv_apply_eq

L40 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_iff_exists_units_of_sectionsOf_equiv_lineBundle.P2mTJ2b.linearEquiv_apply_eq
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_iff_exists_units_of_sectionsOf_equiv_lineBundle
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct Opposite
noncomputable section
namespace P2mTJ2b
section LinAut
variable {B : Type u} [CommRing B]
Lean source · statement
theorem linearEquiv_apply_eq (f : B ≃ₗ[B] B) (x : B) : f x = x * f 1
theorem

isUnit_linearEquiv_one

L43 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_iff_exists_units_of_sectionsOf_equiv_lineBundle.P2mTJ2b.isUnit_linearEquiv_one
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_iff_exists_units_of_sectionsOf_equiv_lineBundle
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct Opposite
noncomputable section
namespace P2mTJ2b
section LinAut
variable {B : Type u} [CommRing B]
Lean source · statement
theorem isUnit_linearEquiv_one (f : B ≃ₗ[B] B) : IsUnit (f 1)
def

isoSections

L59 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_iff_exists_units_of_sectionsOf_equiv_lineBundle.P2mTJ2b.isoSections
Documentation

The linear equivalence on sections induced by an isomorphism of modules.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_iff_exists_units_of_sectionsOf_equiv_lineBundle
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct Opposite
noncomputable section
namespace P2mTJ2b
section IsoSections
variable {X : Scheme.{u}}
Lean source · full declaration
def isoSections {L L' : X.Modules} (φ : L ≅ L') (U : X.Opens) : Γ(L, U) ≃ₗ[Γ(X, U)] Γ(L', U) where
  toFun := φ.hom.app U
  invFun := φ.inv.app U
  map_add' x y := map_add _ x y
  map_smul' r x := Scheme.Modules.Hom.app_smul _ r x
  left_inv x := by
    change (φ.hom.app U ≫ φ.inv.app U) x = x
    rw [← Scheme.Modules.Hom.comp_app, Iso.hom_inv_id, Scheme.Modules.Hom.id_app]; rfl
  right_inv x := by
    change (φ.inv.app U ≫ φ.hom.app U) x = x
    rw [← Scheme.Modules.Hom.comp_app, Iso.inv_hom_id, Scheme.Modules.Hom.id_app]; rfl
theorem

isoSections_apply

L71 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_iff_exists_units_of_sectionsOf_equiv_lineBundle.P2mTJ2b.isoSections_apply
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_iff_exists_units_of_sectionsOf_equiv_lineBundle
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct Opposite
noncomputable section
namespace P2mTJ2b
section IsoSections
variable {X : Scheme.{u}}
Lean source · statement
theorem isoSections_apply {L L' : X.Modules} (φ : L ≅ L') (U : X.Opens) (x : Γ(L, U)) :
    isoSections φ U x = φ.hom.app U x
theorem

app_map

L74 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_iff_exists_units_of_sectionsOf_equiv_lineBundle.P2mTJ2b.app_map
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_iff_exists_units_of_sectionsOf_equiv_lineBundle
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct Opposite
noncomputable section
namespace P2mTJ2b
section IsoSections
variable {X : Scheme.{u}}
Lean source · statement
theorem app_map {M N : X.Modules} (φ : M ⟶ N) {W₁ W₂ : X.Opens} (i : W₁ ⟶ W₂) (x : Γ(M, W₂)) :
    φ.app W₁ (M.presheaf.map i.op x) = N.presheaf.map i.op (φ.app W₂ x)
theorem

exists_units_of_iso

L99 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_iff_exists_units_of_sectionsOf_equiv_lineBundle.P2mTJ2b.exists_units_of_iso
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_iff_exists_units_of_sectionsOf_equiv_lineBundle
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct Opposite
noncomputable section
namespace P2mTJ2b
section Main
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))
variable {L L' : X.Modules}
variable (t t' : (𝒱.cover c).A01ˣ)
variable (e0 : (𝒱.sectionsOf c L).M0 ≃ₗ[(𝒱.cover c).A0] (𝒱.cover c).A0)
  (e1 : (𝒱.sectionsOf c L).M1 ≃ₗ[(𝒱.cover c).A1] (𝒱.cover c).A1)
  (e01 : (𝒱.sectionsOf c L).M01 ≃ₗ[(𝒱.cover c).A01] (𝒱.cover c).A01)
  (he0 : ∀ x, e01 ((𝒱.sectionsOf c L).r0 x) = (𝒱.cover c).ρ0 (e0 x))
  (he1 : ∀ y, e01 ((𝒱.sectionsOf c L).r1 y) = (t : (𝒱.cover c).A01) * (𝒱.cover c).ρ1 (e1 y))
  (e0' : (𝒱.sectionsOf c L').M0 ≃ₗ[(𝒱.cover c).A0] (𝒱.cover c).A0)
  (e1' : (𝒱.sectionsOf c L').M1 ≃ₗ[(𝒱.cover c).A1] (𝒱.cover c).A1)
  (e01' : (𝒱.sectionsOf c L').M01 ≃ₗ[(𝒱.cover c).A01] (𝒱.cover c).A01)
  (he0' : ∀ x, e01' ((𝒱.sectionsOf c L').r0 x) = (𝒱.cover c).ρ0 (e0' x))
  (he1' : ∀ y, e01' ((𝒱.sectionsOf c L').r1 y) = (t' : (𝒱.cover c).A01) * (𝒱.cover c).ρ1 (e1' y))
include he0 he1 he0' he1'
Lean source · statement
theorem exists_units_of_iso (φ : L ≅ L') :
    ∃ (a0 : (𝒱.cover c).A0ˣ) (a1 : (𝒱.cover c).A1ˣ),
      (t' : (𝒱.cover c).A01) =
        (𝒱.cover c).ρ0 (a0 : (𝒱.cover c).A0) * t * (𝒱.cover c).ρ1 ((a1⁻¹ : (𝒱.cover c).A1ˣ) :
          (𝒱.cover c).A1)
theorem

nonempty_iso_of_units

L151 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_iff_exists_units_of_sectionsOf_equiv_lineBundle.P2mTJ2b.nonempty_iso_of_units
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_iff_exists_units_of_sectionsOf_equiv_lineBundle
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct Opposite
noncomputable section
namespace P2mTJ2b
section Main
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))
variable {L L' : X.Modules}
variable (t t' : (𝒱.cover c).A01ˣ)
variable (e0 : (𝒱.sectionsOf c L).M0 ≃ₗ[(𝒱.cover c).A0] (𝒱.cover c).A0)
  (e1 : (𝒱.sectionsOf c L).M1 ≃ₗ[(𝒱.cover c).A1] (𝒱.cover c).A1)
  (e01 : (𝒱.sectionsOf c L).M01 ≃ₗ[(𝒱.cover c).A01] (𝒱.cover c).A01)
  (he0 : ∀ x, e01 ((𝒱.sectionsOf c L).r0 x) = (𝒱.cover c).ρ0 (e0 x))
  (he1 : ∀ y, e01 ((𝒱.sectionsOf c L).r1 y) = (t : (𝒱.cover c).A01) * (𝒱.cover c).ρ1 (e1 y))
  (e0' : (𝒱.sectionsOf c L').M0 ≃ₗ[(𝒱.cover c).A0] (𝒱.cover c).A0)
  (e1' : (𝒱.sectionsOf c L').M1 ≃ₗ[(𝒱.cover c).A1] (𝒱.cover c).A1)
  (e01' : (𝒱.sectionsOf c L').M01 ≃ₗ[(𝒱.cover c).A01] (𝒱.cover c).A01)
  (he0' : ∀ x, e01' ((𝒱.sectionsOf c L').r0 x) = (𝒱.cover c).ρ0 (e0' x))
  (he1' : ∀ y, e01' ((𝒱.sectionsOf c L').r1 y) = (t' : (𝒱.cover c).A01) * (𝒱.cover c).ρ1 (e1' y))
include he0 he1 he0' he1'
Lean source · statement
theorem nonempty_iso_of_units (hL : Scheme.Modules.IsInvertible L) (hL' :
  Scheme.Modules.IsInvertible L')
    (a0 : (𝒱.cover c).A0ˣ) (a1 : (𝒱.cover c).A1ˣ)
    (h : (t' : (𝒱.cover c).A01) =
      (𝒱.cover c).ρ0 (a0 : (𝒱.cover c).A0) * t * (𝒱.cover c).ρ1 ((a1⁻¹ : (𝒱.cover c).A1ˣ) :
        (𝒱.cover c).A1)) :
    Nonempty (L ≅ L')
theorem

nonempty_iso_iff_exists_units_of_sectionsOf_equiv_lineBundle

L210 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.nonempty_iso_iff_exists_units_of_sectionsOf_equiv_lineBundle
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TensorProduct
open _root_.Opposite
open _root_.AlgebraicCurves.Geometry.Schemes.Proofs in
open Scheme_TwoAffineOpenCover_nonempty_iso_iff_exists_units_of_sectionsOf_equiv_lineBundle in
Lean source · statement
theorem nonempty_iso_iff_exists_units_of_sectionsOf_equiv_lineBundle
    {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R))
    {L L' : X.Modules} (hL : Scheme.Modules.IsInvertible L) (hL' : Scheme.Modules.IsInvertible L')
    (t t' : (𝒱.cover c).A01ˣ)
    (e0 : (𝒱.sectionsOf c L).M0 ≃ₗ[(𝒱.cover c).A0] (𝒱.cover c).A0)
    (e1 : (𝒱.sectionsOf c L).M1 ≃ₗ[(𝒱.cover c).A1] (𝒱.cover c).A1)
    (e01 : (𝒱.sectionsOf c L).M01 ≃ₗ[(𝒱.cover c).A01] (𝒱.cover c).A01)
    (he0 : ∀ x, e01 ((𝒱.sectionsOf c L).r0 x) = (𝒱.cover c).ρ0 (e0 x))
    (he1 : ∀ y, e01 ((𝒱.sectionsOf c L).r1 y) = (t : (𝒱.cover c).A01) * (𝒱.cover c).ρ1 (e1 y))
    (e0' : (𝒱.sectionsOf c L').M0 ≃ₗ[(𝒱.cover c).A0] (𝒱.cover c).A0)
    (e1' : (𝒱.sectionsOf c L').M1 ≃ₗ[(𝒱.cover c).A1] (𝒱.cover c).A1)
    (e01' : (𝒱.sectionsOf c L').M01 ≃ₗ[(𝒱.cover c).A01] (𝒱.cover c).A01)
    (he0' : ∀ x, e01' ((𝒱.sectionsOf c L').r0 x) = (𝒱.cover c).ρ0 (e0' x))
    (he1' : ∀ y, e01' ((𝒱.sectionsOf c L').r1 y) = (t' : (𝒱.cover c).A01) * (𝒱.cover c).ρ1 (e1' y))
      :
    Nonempty (L ≅ L') ↔
      ∃ (a0 : (𝒱.cover c).A0ˣ) (a1 : (𝒱.cover c).A1ˣ),
        (t' : (𝒱.cover c).A01) =
          (𝒱.cover c).ρ0 (a0 : (𝒱.cover c).A0) * t * (𝒱.cover c).ρ1 ((a1⁻¹ : (𝒱.cover c).A1ˣ) :
            (𝒱.cover c).A1)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.