NYLL
Module

Scheme_Modules_nonempty_pullback_foldr_twist_iso.lean

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

Module documentation

Scheme Modules nonempty pullback foldr twist iso

Imports10
Imported by4

Declarations

theorem

comap_pow

L66 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_foldr_twist_iso.AlgebraicGeometry.Scheme.IdealSheafData.comap_pow
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_foldr_twist_iso
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
namespace Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y : Scheme.{u}} (f : X ⟶ Y)
Lean source · statement
theorem comap_pow (I : Y.IdealSheafData) (n : ℕ) : (I ^ n).comap f = I.comap f ^ n
theorem

comap_finset_prod

L71 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_foldr_twist_iso.AlgebraicGeometry.Scheme.IdealSheafData.comap_finset_prod
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_foldr_twist_iso
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
namespace Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y : Scheme.{u}} (f : X ⟶ Y)
Lean source · statement
theorem comap_finset_prod {ι : Type*} (s : Finset ι) (I : ι → Y.IdealSheafData) :
    (∏ i ∈ s, I i).comap f = ∏ i ∈ s, (I i).comap f
theorem

finset_prod

L84 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_foldr_twist_iso.AlgebraicGeometry.Scheme.IdealSheafData.IsInvertible.finset_prod
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_foldr_twist_iso
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
namespace Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y : Scheme.{u}} (f : X ⟶ Y)
open scoped _root_.AlgebraicGeometry.Scheme.IdealSheafData.IsInvertible in
Lean source · statement
theorem IsInvertible.finset_prod {ι : Type*} (s : Finset ι) (I : ι → Y.IdealSheafData)
    (hI : ∀ i ∈ s, (I i).IsInvertible) : (∏ i ∈ s, I i).IsInvertible
def

pullbackModuleIso

L97 ↗
AlgebraicGeometry.Scheme.IdealSheafData.IsInvertible.pullbackModuleIso
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_foldr_twist_iso
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
namespace Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y : Scheme.{u}} (f : X ⟶ Y)
namespace IsInvertible
open scoped _root_.AlgebraicGeometry.Scheme.IdealSheafData.IsInvertible in
Lean source · statement
def
  _root_.AlgebraicGeometry.Scheme.IdealSheafData.IsInvertible.pullbackModuleIso {I :
  Y.IdealSheafData} (hI : I.IsInvertible)
    (hI' : (I.comap f).IsInvertible) : (Scheme.Modules.pullback f).obj I.module ≅ (I.comap
      f).module
def

pullbackInvModuleIso

L112 ↗
AlgebraicGeometry.Scheme.IdealSheafData.IsInvertible.pullbackInvModuleIso
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_foldr_twist_iso
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
namespace Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y : Scheme.{u}} (f : X ⟶ Y)
namespace IsInvertible
open scoped _root_.AlgebraicGeometry.Scheme.IdealSheafData.IsInvertible in
Lean source · statement
def
  _root_.AlgebraicGeometry.Scheme.IdealSheafData.IsInvertible.pullbackInvModuleIso {I :
  Y.IdealSheafData} (hI : I.IsInvertible)
    (hI' : (I.comap f).IsInvertible) : (Scheme.Modules.pullback f).obj I.invModule ≅ (I.comap
      f).invModule
theorem

nonempty_pullback_prod_pow_twist_iso

L153 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_foldr_twist_iso.AlgebraicGeometry.Scheme.Modules.nonempty_pullback_prod_pow_twist_iso
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_foldr_twist_iso
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_nonempty_pullback_foldr_twist_iso.AlgebraicGeometry.Scheme.IdealSheafData
variable {X Y : Scheme.{u}} (f : X ⟶ Y)
Lean source · statement
theorem nonempty_pullback_prod_pow_twist_iso {ι : Type*} [Fintype ι] (C : ι → Y.IdealSheafData)
    (aplus aminus : ι → ℕ) (hC : ∀ F, (C F).IsInvertible) (hC' : ∀ F, ((C F).comap f).IsInvertible)
      :
    Nonempty ((Scheme.Modules.pullback f).obj
        ((∏ F, C F ^ aplus F).invModule ⊗ (∏ F, C F ^ aminus F).module) ≅
      (∏ F, (C F).comap f ^ aplus F).invModule ⊗ (∏ F, (C F).comap f ^ aminus F).module)
theorem

nonempty_pullback_foldr_twist_iso

L172 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_foldr_twist_iso.AlgebraicGeometry.Scheme.Modules.nonempty_pullback_foldr_twist_iso
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_foldr_twist_iso
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_nonempty_pullback_foldr_twist_iso.AlgebraicGeometry.Scheme.IdealSheafData
variable {X Y : Scheme.{u}} (f : X ⟶ Y)
Lean source · full declaration
theorem nonempty_pullback_foldr_twist_iso {m : ℕ} (K : Fin m → Y.IdealSheafData) (pos neg : Fin m →
  ℕ)
    {ι : Type*} [Fintype ι] (C : ι → Y.IdealSheafData) (aplus aminus : ι → ℕ)
    (hK : ∀ j, (K j).IsInvertible) (hC : ∀ F, (C F).IsInvertible)
    (hK' : ∀ j, ((K j).comap f).IsInvertible) (hC' : ∀ F, ((C F).comap f).IsInvertible) :
    Nonempty ((Scheme.Modules.pullback f).obj
        ((List.finRange m).foldr (fun j N => (K j ^ pos j).invModule ⊗ (K j ^ neg j).module ⊗ N)
          ((∏ F, C F ^ aplus F).invModule ⊗ (∏ F, C F ^ aminus F).module)) ≅
      (List.finRange m).foldr (fun j N => ((K j).comap f ^ pos j).invModule ⊗ ((K j).comap f ^ neg
        j).module ⊗ N)
        ((∏ F, (C F).comap f ^ aplus F).invModule ⊗ (∏ F, (C F).comap f ^ aminus F).module)) := by
  suffices key : ∀ l : List (Fin m), Nonempty ((Scheme.Modules.pullback f).obj
        (l.foldr (fun j N => (K j ^ pos j).invModule ⊗ (K j ^ neg j).module ⊗ N)
          ((∏ F, C F ^ aplus F).invModule ⊗ (∏ F, C F ^ aminus F).module)) ≅
      l.foldr (fun j N => ((K j).comap f ^ pos j).invModule ⊗ ((K j).comap f ^ neg j).module ⊗ N)
        ((∏ F, (C F).comap f ^ aplus F).invModule ⊗ (∏ F, (C F).comap f ^ aminus F).module)) from
          key _
  intro l
  induction l with
  | nil => exact nonempty_pullback_prod_pow_twist_iso f C aplus aminus hC hC'
  | cons j l ih =>
    obtain ⟨e⟩ := ih
    have hp : ∀ n : ℕ, (K j ^ n).IsInvertible := fun n => IsInvertible.pow (hK j) n
    have hp' : ∀ n : ℕ, ((K j ^ n).comap f).IsInvertible := fun n => by
      rw [comap_pow]; exact IsInvertible.pow (hK' j) n
    simp only [List.foldr_cons]
    exact ⟨pullbackTensorObjIso f _ _ ≪≫
      (((hp (pos j)).pullbackInvModuleIso f (hp' (pos j)) ≪≫
          eqToIso (congrArg Scheme.IdealSheafData.invModule (comap_pow f (K j) (pos j)))) ⊗ᵢ
        (pullbackTensorObjIso f _ _ ≪≫
          (((hp (neg j)).pullbackModuleIso f (hp' (neg j)) ≪≫
              eqToIso (congrArg Scheme.IdealSheafData.module (comap_pow f (K j) (neg j)))) ⊗ᵢ e)))⟩
theorem

nonempty_pullback_foldr_twist_iso

L210 ↗
AlgebraicGeometry.Scheme.Modules.nonempty_pullback_foldr_twist_iso
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_foldr_twist_iso
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules AlgebraicGeometry.Scheme.Modules in
open Scheme_Modules_nonempty_pullback_foldr_twist_iso.AlgebraicGeometry.Scheme.Modules
  renaming nonempty_pullback_foldr_twist_iso → pullbackFoldrTwistProof in
Lean source · full declaration
theorem _root_.AlgebraicGeometry.Scheme.Modules.nonempty_pullback_foldr_twist_iso
    {X Y : Scheme.{u}} (f : X ⟶ Y) {m : ℕ} (K : Fin m → Y.IdealSheafData) (pos neg : Fin m → ℕ)
    {ι : Type*} [Fintype ι] (C : ι → Y.IdealSheafData) (aplus aminus : ι → ℕ)
    (hK : ∀ j, (K j).IsInvertible) (hC : ∀ F, (C F).IsInvertible)
    (hK' : ∀ j, ((K j).comap f).IsInvertible) (hC' : ∀ F, ((C F).comap f).IsInvertible) :
    Nonempty ((Scheme.Modules.pullback f).obj
        ((List.finRange m).foldr (fun j N => (K j ^ pos j).invModule ⊗ (K j ^ neg j).module ⊗ N)
          ((∏ F, C F ^ aplus F).invModule ⊗ (∏ F, C F ^ aminus F).module)) ≅
      (List.finRange m).foldr (fun j N => ((K j).comap f ^ pos j).invModule ⊗ ((K j).comap f ^ neg
        j).module ⊗ N)
        ((∏ F, (C F).comap f ^ aplus F).invModule ⊗ (∏ F, (C F).comap f ^ aminus F).module)) :=
  pullbackFoldrTwistProof f K pos neg C aplus aminus hK hC hK' hC'

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