Module

RigidifiedLineBundle_iso_eq_of_map_pullback_rigSection_comp_eq_of_surjective.lean

Nyll.AlgebraicCurves.Geometry.Picard.RigidifiedLineBundle_iso_eq_of_map_pullback_rigSection_comp_eq_of_surjective

27 declarations indexed from sourceView source ↗

Module documentation

Prove uniqueness of isomorphisms respecting rigidifications when the base-change map on global sections is surjective.

Imports4

Nyll.AlgebraicCurves.Geometry.Schemes.SchemeHomOver
Nyll.AlgebraicCurves.Geometry.Picard.Functor
Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_existsUnique_app_eq_smul
Mathlib.Util.WithWeakNamespace

Imported by2

abbrev

unitModule

L48 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_iso_eq_of_map_pullback_rigSection_comp_eq_of_surjective.AlgebraicGeometry.Scheme.Modules.unitModule

Documentation

The structure sheaf viewed as the unit module.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_iso_eq_of_map_pullback_rigSection_comp_eq_of_surjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y : Scheme.{u}}

Lean source · statement

abbrev unitModule (X : Scheme.{u}) : X.Modules

lemma

app_naturality

L54 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_iso_eq_of_map_pullback_rigSection_comp_eq_of_surjective.AlgebraicGeometry.Scheme.Modules.Hom.app_naturality

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_iso_eq_of_map_pullback_rigSection_comp_eq_of_surjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y : Scheme.{u}}
open scoped _root_.AlgebraicGeometry.Scheme.Modules.Hom in

Lean source · statement

lemma Hom.app_naturality {M N : X.Modules} (φ : M ⟶ N) {U V : X.Opens} (i : U ⟶ V) (x : Γ(M, V)) :
    φ.app U (M.presheaf.map i.op x) = N.presheaf.map i.op (φ.app V x)

abbrev

resTop

L63 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_iso_eq_of_map_pullback_rigSection_comp_eq_of_surjective.AlgebraicGeometry.Scheme.Modules.resTop

Documentation

Restriction of a global function to an open subset.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_iso_eq_of_map_pullback_rigSection_comp_eq_of_surjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y : Scheme.{u}}

Lean source · statement

abbrev resTop (s : Γ(X, ⊤)) (U : X.Opens) : Γ(X, U)

lemma

map_resTop

L66 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_iso_eq_of_map_pullback_rigSection_comp_eq_of_surjective.AlgebraicGeometry.Scheme.Modules.map_resTop

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_iso_eq_of_map_pullback_rigSection_comp_eq_of_surjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y : Scheme.{u}}

Lean source · statement

lemma map_resTop (s : Γ(X, ⊤)) {U V : X.Opens} (i : U ⟶ V) :
    X.presheaf.map i.op (resTop s V) = resTop s U

lemma

resTop_top

L71 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_iso_eq_of_map_pullback_rigSection_comp_eq_of_surjective.AlgebraicGeometry.Scheme.Modules.resTop_top

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_iso_eq_of_map_pullback_rigSection_comp_eq_of_surjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y : Scheme.{u}}

Lean source · statement

lemma resTop_top (s : Γ(X, ⊤)) : resTop s ⊤ = s

lemma

smul_res_comm

L74 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_iso_eq_of_map_pullback_rigSection_comp_eq_of_surjective.AlgebraicGeometry.Scheme.Modules.smul_res_comm

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_iso_eq_of_map_pullback_rigSection_comp_eq_of_surjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y : Scheme.{u}}

Lean source · statement

lemma smul_res_comm (s : Γ(X, ⊤)) (M : X.Modules) (U : X.Opens) (r : Γ(X, U)) (m : Γ(M, U)) :
    resTop s U • r • m = r • resTop s U • m

lemma

map_resTop_smul

L78 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_iso_eq_of_map_pullback_rigSection_comp_eq_of_surjective.AlgebraicGeometry.Scheme.Modules.map_resTop_smul

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_iso_eq_of_map_pullback_rigSection_comp_eq_of_surjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y : Scheme.{u}}

Lean source · statement

lemma map_resTop_smul (s : Γ(X, ⊤)) (M : X.Modules) {U V : X.Opens} (i : U ⟶ V) (x : Γ(M, V)) :
    M.presheaf.map i.op (resTop s V • x) = resTop s U • M.presheaf.map i.op x

def

smulHom

L83 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_iso_eq_of_map_pullback_rigSection_comp_eq_of_surjective.AlgebraicGeometry.Scheme.Modules.smulHom

Documentation

The module endomorphism given by multiplication by a global function.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_iso_eq_of_map_pullback_rigSection_comp_eq_of_surjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y : Scheme.{u}}

Lean source · statement

def smulHom (s : Γ(X, ⊤)) (M : X.Modules) : M ⟶ M

lemma

smulHom_app_apply

L92 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_iso_eq_of_map_pullback_rigSection_comp_eq_of_surjective.AlgebraicGeometry.Scheme.Modules.smulHom_app_apply

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_iso_eq_of_map_pullback_rigSection_comp_eq_of_surjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y : Scheme.{u}}

Lean source · statement

lemma smulHom_app_apply (s : Γ(X, ⊤)) (M : X.Modules) (U : X.Opens) (x : Γ(M, U)) :
    (smulHom s M).app U x = resTop s U • x

lemma

smulHom_comp

L95 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_iso_eq_of_map_pullback_rigSection_comp_eq_of_surjective.AlgebraicGeometry.Scheme.Modules.smulHom_comp

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_iso_eq_of_map_pullback_rigSection_comp_eq_of_surjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y : Scheme.{u}}

Lean source · statement

lemma smulHom_comp (s : Γ(X, ⊤)) {M N : X.Modules} (φ : M ⟶ N) :
    smulHom s M ≫ φ = φ ≫ smulHom s N

lemma

smulHom_mul

L101 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_iso_eq_of_map_pullback_rigSection_comp_eq_of_surjective.AlgebraicGeometry.Scheme.Modules.smulHom_mul

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_iso_eq_of_map_pullback_rigSection_comp_eq_of_surjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y : Scheme.{u}}

Lean source · statement

lemma smulHom_mul (s s' : Γ(X, ⊤)) (M : X.Modules) :
    smulHom (s * s') M = smulHom s' M ≫ smulHom s M

lemma

smulHom_one

L107 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_iso_eq_of_map_pullback_rigSection_comp_eq_of_surjective.AlgebraicGeometry.Scheme.Modules.smulHom_one

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_iso_eq_of_map_pullback_rigSection_comp_eq_of_surjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y : Scheme.{u}}

Lean source · statement

lemma smulHom_one (M : X.Modules) : smulHom (1 : Γ(X, ⊤)) M = 𝟙 M

def

smulIso

L113 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_iso_eq_of_map_pullback_rigSection_comp_eq_of_surjective.AlgebraicGeometry.Scheme.Modules.smulIso

Documentation

The module automorphism given by multiplication by an invertible global function.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_iso_eq_of_map_pullback_rigSection_comp_eq_of_surjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y : Scheme.{u}}

Lean source · full declaration

def smulIso (s : Γ(X, ⊤)ˣ) (M : X.Modules) : M ≅ M where
  hom := smulHom (s : Γ(X, ⊤)) M
  inv := smulHom (↑s⁻¹ : Γ(X, ⊤)) M
  hom_inv_id := by rw [← smulHom_mul, Units.inv_mul, smulHom_one]
  inv_hom_id := by rw [← smulHom_mul, Units.mul_inv, smulHom_one]

def

unitOne

L120 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_iso_eq_of_map_pullback_rigSection_comp_eq_of_surjective.AlgebraicGeometry.Scheme.Modules.unitOne

Documentation

The section one of the unit module on an open subset.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_iso_eq_of_map_pullback_rigSection_comp_eq_of_surjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y : Scheme.{u}}

Lean source · statement

def unitOne (U : X.Opens) : Γ(unitModule X, U)

def

toΓ

L123 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_iso_eq_of_map_pullback_rigSection_comp_eq_of_surjective.AlgebraicGeometry.Scheme.Modules.toΓ

Documentation

View a section of the unit module as a function on the same open subset.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_iso_eq_of_map_pullback_rigSection_comp_eq_of_surjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y : Scheme.{u}}

Lean source · statement

def toΓ {U : X.Opens} (x : Γ(unitModule X, U)) : Γ(X, U)

lemma

eq_toΓ_smul_unitOne

L125 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_iso_eq_of_map_pullback_rigSection_comp_eq_of_surjective.AlgebraicGeometry.Scheme.Modules.eq_toΓ_smul_unitOne

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_iso_eq_of_map_pullback_rigSection_comp_eq_of_surjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y : Scheme.{u}}

Lean source · statement

lemma eq_toΓ_smul_unitOne {U : X.Opens} (x : Γ(unitModule X, U)) : x = toΓ x • unitOne U

lemma

map_unitOne

L128 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_iso_eq_of_map_pullback_rigSection_comp_eq_of_surjective.AlgebraicGeometry.Scheme.Modules.map_unitOne

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_iso_eq_of_map_pullback_rigSection_comp_eq_of_surjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y : Scheme.{u}}

Lean source · statement

lemma map_unitOne {U V : X.Opens} (i : U ⟶ V) :
    (unitModule X).presheaf.map i.op (unitOne V) = unitOne U

lemma

smulHom_app_top_one

L132 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_iso_eq_of_map_pullback_rigSection_comp_eq_of_surjective.AlgebraicGeometry.Scheme.Modules.smulHom_app_top_one

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_iso_eq_of_map_pullback_rigSection_comp_eq_of_surjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y : Scheme.{u}}

Lean source · statement

lemma smulHom_app_top_one (u : unitModule X ⟶ unitModule X) :
    smulHom (u.app ⊤ (unitOne ⊤)) (unitModule X) = u

lemma

app_top_comp_unitOne

L145 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_iso_eq_of_map_pullback_rigSection_comp_eq_of_surjective.AlgebraicGeometry.Scheme.Modules.app_top_comp_unitOne

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_iso_eq_of_map_pullback_rigSection_comp_eq_of_surjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y : Scheme.{u}}

Lean source · statement

lemma app_top_comp_unitOne (u v : unitModule X ⟶ unitModule X) :
    toΓ ((u ≫ v).app ⊤ (unitOne ⊤)) = toΓ (u.app ⊤ (unitOne ⊤)) * toΓ (v.app ⊤ (unitOne ⊤))

def

unitOfAut

L153 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_iso_eq_of_map_pullback_rigSection_comp_eq_of_surjective.AlgebraicGeometry.Scheme.Modules.unitOfAut

Documentation

The invertible global function associated to an automorphism of the unit module.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_iso_eq_of_map_pullback_rigSection_comp_eq_of_surjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y : Scheme.{u}}

Lean source · full declaration

def unitOfAut (δ : unitModule X ≅ unitModule X) : Γ(X, ⊤)ˣ where
  val := toΓ (δ.hom.app ⊤ (unitOne ⊤))
  inv := toΓ (δ.inv.app ⊤ (unitOne ⊤))
  val_inv := by rw [← app_top_comp_unitOne, δ.hom_inv_id]; rfl
  inv_val := by rw [← app_top_comp_unitOne, δ.inv_hom_id]; rfl

lemma

smulIso_unitOfAut

L159 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_iso_eq_of_map_pullback_rigSection_comp_eq_of_surjective.AlgebraicGeometry.Scheme.Modules.smulIso_unitOfAut

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_iso_eq_of_map_pullback_rigSection_comp_eq_of_surjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y : Scheme.{u}}

Lean source · statement

lemma smulIso_unitOfAut (δ : unitModule X ≅ unitModule X) :
    smulIso (unitOfAut δ) (unitModule X) = δ

lemma

resTop_appTop

L164 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_iso_eq_of_map_pullback_rigSection_comp_eq_of_surjective.AlgebraicGeometry.Scheme.Modules.resTop_appTop

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_iso_eq_of_map_pullback_rigSection_comp_eq_of_surjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y : Scheme.{u}}

Lean source · statement

lemma resTop_appTop (f : X ⟶ Y) (s : Γ(Y, ⊤)) (U : Y.Opens) :
    resTop (f.appTop s) (f ⁻¹ᵁ U) = f.app U (resTop s U)

lemma

pushforward_map_smulHom

L169 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_iso_eq_of_map_pullback_rigSection_comp_eq_of_surjective.AlgebraicGeometry.Scheme.Modules.pushforward_map_smulHom

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_iso_eq_of_map_pullback_rigSection_comp_eq_of_surjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y : Scheme.{u}}

Lean source · statement

lemma pushforward_map_smulHom (f : X ⟶ Y) (s : Γ(Y, ⊤)) (P : X.Modules) :
    (pushforward f).map (smulHom (f.appTop s) P) = smulHom s ((pushforward f).obj P)

lemma

pullback_map_smulHom

L176 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_iso_eq_of_map_pullback_rigSection_comp_eq_of_surjective.AlgebraicGeometry.Scheme.Modules.pullback_map_smulHom

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_iso_eq_of_map_pullback_rigSection_comp_eq_of_surjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y : Scheme.{u}}

Lean source · statement

lemma pullback_map_smulHom (f : X ⟶ Y) (s : Γ(Y, ⊤)) (M : Y.Modules) :
    (Scheme.Modules.pullback f).map (smulHom s M) =
      smulHom (f.appTop s) ((Scheme.Modules.pullback f).obj M)

lemma

pullback_mapIso_smulIso

L186 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_iso_eq_of_map_pullback_rigSection_comp_eq_of_surjective.AlgebraicGeometry.Scheme.Modules.pullback_mapIso_smulIso

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_iso_eq_of_map_pullback_rigSection_comp_eq_of_surjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y : Scheme.{u}}

Lean source · statement

lemma pullback_mapIso_smulIso (f : X ⟶ Y) (s : Γ(Y, ⊤)ˣ) (M : Y.Modules) :
    (Scheme.Modules.pullback f).mapIso (smulIso s M) =
      smulIso (Units.map (f.appTop).hom.toMonoidHom s) ((Scheme.Modules.pullback f).obj M)

lemma

appTop_appTop_of_comp_eq_id

L192 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_iso_eq_of_map_pullback_rigSection_comp_eq_of_surjective.AlgebraicGeometry.Scheme.Modules.appTop_appTop_of_comp_eq_id

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_iso_eq_of_map_pullback_rigSection_comp_eq_of_surjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y : Scheme.{u}}

Lean source · statement

lemma appTop_appTop_of_comp_eq_id {T P : Scheme.{u}} (e : T ⟶ P) (p : P ⟶ T) (h : e ≫ p = 𝟙 T)
    (d : Γ(T, ⊤)) :
    e.appTop (p.appTop d) = d

theorem

iso_eq_of_map_pullback_rigSection_comp_eq_of_surjective

L210 ↗

AlgebraicGeometry.RelPicard.RigidifiedLineBundle.iso_eq_of_map_pullback_rigSection_comp_eq_of_surjective

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_iso_eq_of_map_pullback_rigSection_comp_eq_of_surjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.Scheme.Modules in
with_weak_namespace AlgebraicGeometry.Scheme
open Modules in
with_weak_namespace _root_.AlgebraicGeometry.RelPicard.RigidifiedLineBundle

Lean source · statement

theorem iso_eq_of_map_pullback_rigSection_comp_eq_of_surjective
    (R : Type u) [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
    {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))
    (hp : Function.Surjective (pullback.snd c t).appTop)
    (M M' : RigidifiedLineBundle c ε t)
    (α : (Scheme.Modules.pullback (rigSection c t ε)).obj M.L ≅ SheafOfModules.unit T.ringCatSheaf)
    (α' : (Scheme.Modules.pullback (rigSection c t ε)).obj M'.L ≅ SheafOfModules.unit
      T.ringCatSheaf)
    (φ ψ : M.L ≅ M'.L)
    (hφ : (Scheme.Modules.pullback (rigSection c t ε)).mapIso φ ≪≫ α' = α)
    (hψ : (Scheme.Modules.pullback (rigSection c t ε)).mapIso ψ ≪≫ α' = α) :
    φ = ψ

Module documentation

Declarations