NYLL
Module

Scheme_Modules_unitAutSection_trans_and_unitAutSection_refl.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_unitAutSection_trans_and_unitAutSection_refl
11 declarations indexed from sourceView source ↗

Module documentation

Scheme Modules unit Aut Section trans and unit Aut Section refl

Imports5
Imported by6

Declarations

def

uapp

L59 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutomorphisms.AlgebraicGeometry.Scheme.Modules.uapp
Documentation

The action of a unit-sheaf automorphism on global sections of the open subscheme.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutomorphisms
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {Y : Scheme.{u}}
Lean source · statement
def uapp (W : Y.Opens)
    (e : SheafOfModules.unit (W : Scheme.{u}).ringCatSheaf ≅ SheafOfModules.unit (W :
      Scheme.{u}).ringCatSheaf)
    (x : (W : Scheme.{u}).presheaf.obj (op ⊤)) : (W : Scheme.{u}).presheaf.obj (op ⊤)
theorem

unitAutSection_eq

L65 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutomorphisms.AlgebraicGeometry.Scheme.Modules.unitAutSection_eq
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutomorphisms
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {Y : Scheme.{u}}
Lean source · statement
theorem unitAutSection_eq (W : Y.Opens)
    (e : SheafOfModules.unit (W : Scheme.{u}).ringCatSheaf ≅ SheafOfModules.unit (W :
      Scheme.{u}).ringCatSheaf) :
    unitAutSection W e = W.topIso.hom.hom (uapp W e 1)
theorem

uapp_mul

L70 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutomorphisms.AlgebraicGeometry.Scheme.Modules.uapp_mul
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutomorphisms
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {Y : Scheme.{u}}
Lean source · statement
theorem uapp_mul (W : Y.Opens)
    (e : SheafOfModules.unit (W : Scheme.{u}).ringCatSheaf ≅ SheafOfModules.unit (W :
      Scheme.{u}).ringCatSheaf)
    (x y : (W : Scheme.{u}).presheaf.obj (op ⊤)) : uapp W e (x * y) = x * uapp W e y
theorem

uapp_trans

L77 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutomorphisms.AlgebraicGeometry.Scheme.Modules.uapp_trans
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutomorphisms
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {Y : Scheme.{u}}
Lean source · statement
theorem uapp_trans (W : Y.Opens)
    (e e' : SheafOfModules.unit (W : Scheme.{u}).ringCatSheaf ≅ SheafOfModules.unit (W :
      Scheme.{u}).ringCatSheaf)
    (x : (W : Scheme.{u}).presheaf.obj (op ⊤)) : uapp W (e ≪≫ e') x = uapp W e' (uapp W e x)
theorem

uapp_refl

L84 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutomorphisms.AlgebraicGeometry.Scheme.Modules.uapp_refl
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutomorphisms
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {Y : Scheme.{u}}
Lean source · statement
theorem uapp_refl (W : Y.Opens) (x : (W : Scheme.{u}).presheaf.obj (op ⊤)) : uapp W (Iso.refl _) x
  = x
theorem

unitAutSection_trans

L89 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutomorphisms.AlgebraicGeometry.Scheme.Modules.unitAutSection_trans
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutomorphisms
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {Y : Scheme.{u}}
Lean source · statement
theorem unitAutSection_trans (W : Y.Opens)
    (e e' : SheafOfModules.unit (W : Scheme.{u}).ringCatSheaf ≅ SheafOfModules.unit (W :
      Scheme.{u}).ringCatSheaf) :
    unitAutSection W (e ≪≫ e') = unitAutSection W e * unitAutSection W e'
theorem

unitAutSection_refl

L96 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutomorphisms.AlgebraicGeometry.Scheme.Modules.unitAutSection_refl
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutomorphisms
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {Y : Scheme.{u}}
Lean source · statement
theorem unitAutSection_refl (W : Y.Opens) :
    unitAutSection W (Iso.refl _) = 1
theorem

unitAutSection_symm_mul

L100 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutomorphisms.AlgebraicGeometry.Scheme.Modules.unitAutSection_symm_mul
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutomorphisms
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {Y : Scheme.{u}}
Lean source · statement
theorem unitAutSection_symm_mul (W : Y.Opens)
    (e : SheafOfModules.unit (W : Scheme.{u}).ringCatSheaf ≅ SheafOfModules.unit (W :
      Scheme.{u}).ringCatSheaf) :
    unitAutSection W e.symm * unitAutSection W e = 1
theorem

unitAutSection_mul_symm

L106 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutomorphisms.AlgebraicGeometry.Scheme.Modules.unitAutSection_mul_symm
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutomorphisms
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {Y : Scheme.{u}}
Lean source · statement
theorem unitAutSection_mul_symm (W : Y.Opens)
    (e : SheafOfModules.unit (W : Scheme.{u}).ringCatSheaf ≅ SheafOfModules.unit (W :
      Scheme.{u}).ringCatSheaf) :
    unitAutSection W e * unitAutSection W e.symm = 1
theorem

isUnit_unitAutSection

L112 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutomorphisms.AlgebraicGeometry.Scheme.Modules.isUnit_unitAutSection
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutomorphisms
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {Y : Scheme.{u}}
Lean source · statement
theorem isUnit_unitAutSection (W : Y.Opens)
    (e : SheafOfModules.unit (W : Scheme.{u}).ringCatSheaf ≅ SheafOfModules.unit (W :
      Scheme.{u}).ringCatSheaf) :
    IsUnit (unitAutSection W e)
theorem

unitAutSection_trans_and_unitAutSection_refl

L120 ↗
AlgebraicGeometry.Scheme.Modules.unitAutSection_trans_and_unitAutSection_refl
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutomorphisms
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.Modules.unitAutSection_trans_and_unitAutSection_refl
    {Y : Scheme.{u}} (W : Y.Opens) :
    (∀ e e' : SheafOfModules.unit (W : Scheme.{u}).ringCatSheaf ≅ SheafOfModules.unit (W :
      Scheme.{u}).ringCatSheaf,
        Scheme.Modules.unitAutSection W (e ≪≫ e') =
          Scheme.Modules.unitAutSection W e * Scheme.Modules.unitAutSection W e') ∧
      Scheme.Modules.unitAutSection W (Iso.refl _) = 1

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