NYLL
Module

Scheme_Modules_isIso_projectionMorphism_of_iso_free.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_isIso_projectionMorphism_of_iso_free
8 declarations indexed from sourceView source ↗

Module documentation

Projection morphisms for finite free module sheaves

The projection morphism is an isomorphism for a finite free module, using its biproduct presentation and compatibility with module isomorphisms.

Imports5
Imported by4

Declarations

lemma

isIso_of_iso

L53 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_projectionMorphism_of_iso_free.AlgebraicGeometry.Scheme.Modules.PFFree.isIso_of_iso
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_projectionMorphism_of_iso_free
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
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
namespace PFFree
variable {Z X : Scheme.{u}} (i : Z ⟶ X)
Lean source · statement
lemma isIso_of_iso {F F' : X.Modules} (e : F ≅ F') (h : IsIso (projectionMorphism i F')) :
    IsIso (projectionMorphism i F)
lemma

mate_unit

L72 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_projectionMorphism_of_iso_free.AlgebraicGeometry.Scheme.Modules.PFFree.mate_unit
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_projectionMorphism_of_iso_free
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
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
namespace PFFree
variable {Z X : Scheme.{u}} (i : Z ⟶ X)
Lean source · statement
lemma mate_unit :
    projectionMorphismMate i (𝟙_ X.Modules) =
      (Modules.pullback i).map ((ρ_ ((Modules.pushforward i).obj (𝟙_ Z.Modules))).hom ≫
          (Modules.pushforward i).map (Functor.Monoidal.εIso (Modules.pullback i)).hom) ≫
        (pullbackPushforwardAdjunction i).counit.app ((Modules.pullback i).obj (𝟙_ X.Modules))
lemma

projectionMorphism_unit

L132 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_projectionMorphism_of_iso_free.AlgebraicGeometry.Scheme.Modules.PFFree.projectionMorphism_unit
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_projectionMorphism_of_iso_free
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
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
namespace PFFree
variable {Z X : Scheme.{u}} (i : Z ⟶ X)
Lean source · statement
lemma projectionMorphism_unit :
    projectionMorphism i (𝟙_ X.Modules) =
      (ρ_ ((Modules.pushforward i).obj (𝟙_ Z.Modules))).hom ≫
        (Modules.pushforward i).map (Functor.Monoidal.εIso (Modules.pullback i)).hom
lemma

isIso_unit

L142 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_projectionMorphism_of_iso_free.AlgebraicGeometry.Scheme.Modules.PFFree.isIso_unit
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_projectionMorphism_of_iso_free
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
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
namespace PFFree
variable {Z X : Scheme.{u}} (i : Z ⟶ X)
Lean source · statement
lemma isIso_unit : IsIso (projectionMorphism i (𝟙_ X.Modules))
abbrev

fam

L154 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_projectionMorphism_of_iso_free.AlgebraicGeometry.Scheme.Modules.PFFree.fam
Documentation

The constant family of n copies of the unit module sheaf on X.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_projectionMorphism_of_iso_free
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
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
namespace PFFree
variable {Z X : Scheme.{u}} (i : Z ⟶ X)
section biproduct
variable (n : ℕ)
Lean source · statement
abbrev fam (X : Scheme.{u}) (n : ℕ) : Fin n → X.Modules
lemma

isIso_biproduct

L156 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_projectionMorphism_of_iso_free.AlgebraicGeometry.Scheme.Modules.PFFree.isIso_biproduct
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_projectionMorphism_of_iso_free
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
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
namespace PFFree
variable {Z X : Scheme.{u}} (i : Z ⟶ X)
section biproduct
variable (n : ℕ)
Lean source · statement
lemma isIso_biproduct [HasFiniteBiproducts X.Modules] :
    IsIso (projectionMorphism i (⨁ fam X n))
theorem

main

L209 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_projectionMorphism_of_iso_free.AlgebraicGeometry.Scheme.Modules.PFFree.main
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_projectionMorphism_of_iso_free
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
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
namespace PFFree
variable {Z X : Scheme.{u}} (i : Z ⟶ X)
Lean source · statement
theorem main {n : ℕ} (F : X.Modules) (e : F ≅ SheafOfModules.free.{u} (ULift.{u} (Fin n))) :
    IsIso (projectionMorphism i F)
theorem

isIso_projectionMorphism_of_iso_free

L221 ↗
AlgebraicGeometry.Scheme.Modules.isIso_projectionMorphism_of_iso_free
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_projectionMorphism_of_iso_free
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.Modules.isIso_projectionMorphism_of_iso_free
    {Z X : Scheme.{u}} (i : Z ⟶ X) {n : ℕ} (F : X.Modules)
    (e : F ≅ SheafOfModules.free.{u} (ULift.{u} (Fin n))) :
    IsIso (Scheme.Modules.projectionMorphism i F)

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