Module

Polarisation_LocIsoOnBase_equivalence.lean

Nyll.AlgebraicCurves.Geometry.Picard.Polarisation_LocIsoOnBase_equivalence

5 declarations indexed from sourceView source ↗

Module documentation

Polarisation Loc Iso On Base equivalence

Imports3

Mathlib.AlgebraicGeometry.Modules.Sheaf
Mathlib.AlgebraicGeometry.Restrict
Nyll.AlgebraicCurves.Geometry.Picard.PolarisationRosati

Imported by5

theorem

refl

L43 ↗

AlgebraicCurves.Geometry.Picard.Proofs.Polarisation_LocIsoOnBase_equivalence.LocIsoOnBaseEquivSol.refl

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs.Polarisation_LocIsoOnBase_equivalence
noncomputable section
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Polarisation
universe u
namespace LocIsoOnBaseEquivSol
open _root_.AlgebraicGeometry.Polarisation
open _root_.AlgebraicGeometry
variable {S : Type u} [CommRing S] {X : Scheme.{u}} (g : X ⟶ Spec (CommRingCat.of S))

Lean source · statement

theorem refl (M : X.Modules) : LocIsoOnBase g M M

theorem

symm

L47 ↗

AlgebraicCurves.Geometry.Picard.Proofs.Polarisation_LocIsoOnBase_equivalence.LocIsoOnBaseEquivSol.symm

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs.Polarisation_LocIsoOnBase_equivalence
noncomputable section
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Polarisation
universe u
namespace LocIsoOnBaseEquivSol
open _root_.AlgebraicGeometry.Polarisation
open _root_.AlgebraicGeometry
variable {S : Type u} [CommRing S] {X : Scheme.{u}} (g : X ⟶ Spec (CommRingCat.of S))
variable {g} in

Lean source · statement

theorem symm {M M' : X.Modules} (h : LocIsoOnBase g M M') : LocIsoOnBase g M' M

def

restrictIso

L53 ↗

AlgebraicCurves.Geometry.Picard.Proofs.Polarisation_LocIsoOnBase_equivalence.LocIsoOnBaseEquivSol.restrictIso

Documentation

The restriction of a local module isomorphism to a smaller open of the base.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs.Polarisation_LocIsoOnBase_equivalence
noncomputable section
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Polarisation
universe u
namespace LocIsoOnBaseEquivSol
open _root_.AlgebraicGeometry.Polarisation
open _root_.AlgebraicGeometry
variable {S : Type u} [CommRing S] {X : Scheme.{u}} (g : X ⟶ Spec (CommRingCat.of S))
variable {g} in

Lean source · statement

def restrictIso {M M' : X.Modules} {U V : (Spec (CommRingCat.of S)).Opens} (hVU : V ≤ U)
    (e : (Scheme.Modules.pullback (g ⁻¹ᵁ U).ι).obj M ≅ (Scheme.Modules.pullback (g ⁻¹ᵁ U).ι).obj
      M') :
    (Scheme.Modules.pullback (g ⁻¹ᵁ V).ι).obj M ≅ (Scheme.Modules.pullback (g ⁻¹ᵁ V).ι).obj M'

theorem

trans

L65 ↗

AlgebraicCurves.Geometry.Picard.Proofs.Polarisation_LocIsoOnBase_equivalence.LocIsoOnBaseEquivSol.trans

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs.Polarisation_LocIsoOnBase_equivalence
noncomputable section
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Polarisation
universe u
namespace LocIsoOnBaseEquivSol
open _root_.AlgebraicGeometry.Polarisation
open _root_.AlgebraicGeometry
variable {S : Type u} [CommRing S] {X : Scheme.{u}} (g : X ⟶ Spec (CommRingCat.of S))
variable {g} in
variable {g} in

Lean source · statement

theorem trans {M M' M'' : X.Modules} (h : LocIsoOnBase g M M') (h' : LocIsoOnBase g M' M'') :
    LocIsoOnBase g M M''

theorem

equivalence

L75 ↗

AlgebraicGeometry.Polarisation.LocIsoOnBase.equivalence

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs.Polarisation_LocIsoOnBase_equivalence
noncomputable section
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Polarisation
universe u
open LocIsoOnBaseEquivSol in

Lean source · statement

theorem _root_.AlgebraicGeometry.Polarisation.LocIsoOnBase.equivalence
    {S : Type u} [CommRing S] {X : Scheme.{u}} (g : X ⟶ Spec (CommRingCat.of S)) :
    Equivalence (LocIsoOnBase g)

Module documentation

Polarisation Loc Iso On Base equivalence

Declarations

refl

symm

restrictIso

trans

equivalence