NYLL
Module

Scheme_Modules_exists_linearEquiv_sections_pullback_of_isClosedImmersion_of_locallyTrivial.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_linearEquiv_sections_pullback_of_isClosedImmersion_of_locallyTrivial
67 declarations indexed from sourceView source ↗

Module documentation

Sections after pullback along a closed immersion

Local triviality identifies pulled-back sections with scalar extension on affine opens.

Imports10
Imported by1

Declarations

abbrev

iU

L87 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.iU
Documentation

The affine chart associated to an affine open subset.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U)
Lean source · statement
abbrev iU : Spec Γ(X, U) ⟶ X
abbrev

j

L90 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.j
Documentation

The affine chart over the inverse image of an affine open.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U)
Lean source · statement
abbrev j : Spec Γ(Y, i ⁻¹ᵁ U) ⟶ Y
theorem

j_i'

L92 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.j_i'
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U)
Lean source · statement
theorem j_i' : j i U hU ≫ i = Spec.map (i.app U) ≫ iU U hU
theorem

j_i

L96 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.j_i
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U)
Lean source · statement
theorem j_i : j i U hU ≫ i = Spec.map (i.app U) ≫ iU U hU
theorem

le_opensRange_j

L100 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.le_opensRange_j
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U)
Lean source · statement
theorem le_opensRange_j : i ⁻¹ᵁ U ≤ (j i U hU).opensRange
theorem

top_le_preimage_j

L103 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.top_le_preimage_j
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U)
Lean source · statement
theorem top_le_preimage_j : (⊤ : (Spec Γ(Y, i ⁻¹ᵁ U)).Opens) ≤ (j i U hU) ⁻¹ᵁ (i ⁻¹ᵁ U)
theorem

top_le_preimage_iU

L106 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.top_le_preimage_iU
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U)
Lean source · statement
theorem top_le_preimage_iU : (⊤ : (Spec Γ(X, U)).Opens) ≤ (iU U hU) ⁻¹ᵁ U
theorem

unit_app_comp

L151 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.UnitCalculus.unit_app_comp
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace UnitCalculus
variable {X Y Z : Scheme.{u}}
Lean source · statement
theorem unit_app_comp (g : Z ⟶ Y) (f : Y ⟶ X) (M : X.Modules) (U : X.Opens) :
    ((pullbackPushforwardAdjunction (g ≫ f)).unit.app M).app U ≫
        ((pullbackComp g f).inv.app M).app ((g ≫ f) ⁻¹ᵁ U) =
      ((pullbackPushforwardAdjunction f).unit.app M).app U ≫
        ((pullbackPushforwardAdjunction g).unit.app ((Scheme.Modules.pullback f).obj M)).app (f ⁻¹ᵁ
          U)
theorem

unit_app_congr_res

L168 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.UnitCalculus.unit_app_congr_res
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace UnitCalculus
variable {X Y Z : Scheme.{u}}
Lean source · statement
theorem unit_app_congr_res {p₁ p₂ : Z ⟶ X} (h : p₁ = p₂) (M : X.Modules) (U : X.Opens) (W : Z.Opens)
    (hW₁ : W ≤ p₁ ⁻¹ᵁ U) (hW₂ : W ≤ p₂ ⁻¹ᵁ U) :
    ((pullbackPushforwardAdjunction p₁).unit.app M).app U ≫ ((pullbackCongr h).hom.app M).app (p₁
      ⁻¹ᵁ U) ≫
        ((Scheme.Modules.pullback p₂).obj M).presheaf.map (homOfLE hW₁).op =
      ((pullbackPushforwardAdjunction p₂).unit.app M).app U ≫
        ((Scheme.Modules.pullback p₂).obj M).presheaf.map (homOfLE hW₂).op
theorem

bijective_unit_app_of_isOpenImmersion

L179 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.UnitCalculus.bijective_unit_app_of_isOpenImmersion
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace UnitCalculus
variable {X Y Z : Scheme.{u}}
Lean source · statement
theorem bijective_unit_app_of_isOpenImmersion (j : Y ⟶ X) [IsOpenImmersion j] (N : X.Modules)
    (V : X.Opens) (hV : V ≤ j.opensRange) :
    Function.Bijective (((pullbackPushforwardAdjunction j).unit.app N).app V)
abbrev

M'

L253 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.M'
Documentation

The module pulled back to the affine chart.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U) (M : X.Modules)
Lean source · statement
abbrev M' : (Spec Γ(X, U)).Modules
abbrev

MY

L256 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.MY
Documentation

The module pulled back along the given morphism.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U) (M : X.Modules)
Lean source · statement
abbrev MY : Y.Modules
def

η

L259 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.η
Documentation

The section map induced by the pullback adjunction unit.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U) (M : X.Modules)
Lean source · statement
def η : Γ(M, U) ⟶ Γ(MY i M, i ⁻¹ᵁ U)
def

ρ

L263 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.ρ
Documentation

The section map to the affine chart.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U) (M : X.Modules)
Lean source · statement
def ρ : Γ(M, U) ⟶ Γ(M' U hU M, ⊤)
def

θ

L268 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.θ
Documentation

The comparison of sections after pulling back to the affine chart.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U) (M : X.Modules)
Lean source · statement
def θ : Γ(MY i M, i ⁻¹ᵁ U) ⟶
    Γ((Scheme.Modules.pullback (j i U hU)).obj (MY i M), ⊤)
theorem

isIso_presheaf_map_top_le

L274 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.isIso_presheaf_map_top_le
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U) (M : X.Modules)
Lean source · statement
theorem isIso_presheaf_map_top_le {Y : Scheme.{u}} (N : Y.Modules) (V : Y.Opens) (h : (⊤ : Y.Opens)
  ≤ V) :
    IsIso (N.presheaf.map (homOfLE h).op)
theorem

bijective_ρ

L282 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.bijective_ρ
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U) (M : X.Modules)
Lean source · statement
theorem bijective_ρ : Function.Bijective (ρ U hU M)
theorem

bijective_θ

L292 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.bijective_θ
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U) (M : X.Modules)
Lean source · statement
theorem bijective_θ : Function.Bijective (θ i U hU M)
def

σ

L305 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.σ
Documentation

The comparison of the two composite pullbacks.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U) (M : X.Modules)
Lean source · statement
def σ : (Scheme.Modules.pullback (Spec.map (i.app U))).obj (M' U hU M) ≅
    (Scheme.Modules.pullback (j i U hU)).obj (MY i M)
def

ηφ

L312 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.ηφ
Documentation

The adjunction unit on the affine chart.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U) (M : X.Modules)
Lean source · statement
def ηφ : Γ(M' U hU M, ⊤) ⟶ Γ((Scheme.Modules.pullback (Spec.map (i.app U))).obj (M' U hU M), ⊤)
theorem

app_res

L315 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.app_res
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U) (M : X.Modules)
Lean source · statement
theorem app_res {Y : Scheme.{u}} {N₁ N₂ : Y.Modules} (ψ : N₁ ⟶ N₂) {V W : Y.Opens} (h : W ≤ V) (x :
  Γ(N₁, V)) :
    ψ.app W (N₁.presheaf.map (homOfLE h).op x) = N₂.presheaf.map (homOfLE h).op (ψ.app V x)
theorem

hom_inv_app_apply

L321 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.hom_inv_app_apply
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U) (M : X.Modules)
Lean source · statement
theorem hom_inv_app_apply {Y : Scheme.{u}} {N₁ N₂ : Y.Modules} (e : N₁ ≅ N₂) (V : Y.Opens) (x :
  Γ(N₂, V)) :
    e.hom.app V (e.inv.app V x) = x
theorem

σ_hom_app

L328 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.σ_hom_app
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U) (M : X.Modules)
Lean source · statement
theorem σ_hom_app (V : (Spec Γ(Y, i ⁻¹ᵁ U)).Opens)
    (x : Γ((Scheme.Modules.pullback (Spec.map (i.app U))).obj (M' U hU M), V)) :
    (σ i U hU M).hom.app V x =
      ((pullbackComp (j i U hU) i).inv.app M).app V
        (((pullbackCongr (j_i i U hU).symm).hom.app M).app V
          (((pullbackComp (Spec.map (i.app U)) (iU U hU)).hom.app M).app V x))
theorem

le1

L337 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.le1
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U) (M : X.Modules)
omit [IsAffineHom i] in
Lean source · statement
theorem le1 : (⊤ : (Spec Γ(Y, i ⁻¹ᵁ U)).Opens) ≤ (Spec.map (i.app U)) ⁻¹ᵁ ((iU U hU) ⁻¹ᵁ U)
theorem

chase

L340 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.chase
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U) (M : X.Modules)
Lean source · statement
theorem chase (m : Γ(M, U)) :
    ((σ i U hU M).hom.app ⊤) (ηφ i U hU M (ρ U hU M m)) = θ i U hU M (η i U M m)
def

pullbackUnitIso'

L445 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.pullbackUnitIso'
Documentation

The canonical pullback identification for the unit module.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U) (M : X.Modules)
Lean source · statement
def pullbackUnitIso' {Y Z : Scheme.{u}} (f : Y ⟶ Z) :
    (Scheme.Modules.pullback f).obj (SheafOfModules.unit Z.ringCatSheaf) ≅
      SheafOfModules.unit Y.ringCatSheaf
theorem

locallyTrivial_pullback

L450 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.locallyTrivial_pullback
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U) (M : X.Modules)
Lean source · statement
theorem locallyTrivial_pullback {Y Z : Scheme.{u}} (f : Y ⟶ Z) (L : Z.Modules)
    (htriv : ∀ z : Z, ∃ (V : Z.Opens), z ∈ V ∧
      Nonempty ((Scheme.Modules.pullback V.ι).obj L ≅ SheafOfModules.unit V.toScheme.ringCatSheaf))
        :
    ∀ y : Y, ∃ (V : Y.Opens), y ∈ V ∧
      Nonempty ((Scheme.Modules.pullback V.ι).obj ((Scheme.Modules.pullback f).obj L) ≅
        SheafOfModules.unit V.toScheme.ringCatSheaf)
abbrev

N'

L469 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.N'
Documentation

The module of sections represented on the affine chart.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U) (M : X.Modules)
Lean source · statement
abbrev N' : ModuleCat Γ(X, U)
theorem

N'_smul_def

L471 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.N'_smul_def
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U) (M : X.Modules)
Lean source · full declaration
theorem N'_smul_def (b : Γ(X, U)) (n : N' U hU M) :
    b • n = (((Spec Γ(X, U)).presheaf.map (homOfLE (le_top : (⊤ : (Spec Γ(X, U)).Opens) ≤
      ⊤)).op).hom
      ((StructureSheaf.globalSectionsIso Γ(X, U)).hom.hom b)) • (show Γ(M' U hU M, ⊤) from n) := rfl
theorem

res_top_top'

L477 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.res_top_top'
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U) (M : X.Modules)
omit hU M in
Lean source · statement
theorem res_top_top' (s : Γ(Spec Γ(X, U), ⊤)) :
    ((Spec Γ(X, U)).presheaf.map (homOfLE (le_top : (⊤ : (Spec Γ(X, U)).Opens) ≤ ⊤)).op).hom s = s
theorem

iU_appLE

L484 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.iU_appLE
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U) (M : X.Modules)
Lean source · statement
theorem iU_appLE (b : Γ(X, U)) :
    ((Spec Γ(X, U)).presheaf.map (homOfLE (top_le_preimage_iU U hU)).op).hom (((iU U hU).app U).hom
      b)
      = (Scheme.ΓSpecIso Γ(X, U)).inv.hom b
theorem

N'_smul_def'

L500 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.N'_smul_def'
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U) (M : X.Modules)
Lean source · full declaration
theorem N'_smul_def' (b : Γ(X, U)) (n : N' U hU M) :
    b • n = ((Scheme.ΓSpecIso Γ(X, U)).inv.hom b) • (show Γ(M' U hU M, ⊤) from n) := by
  rw [N'_smul_def]
  erw [res_top_top']
theorem

unit_iU_smul

L505 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.unit_iU_smul
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U) (M : X.Modules)
Lean source · full declaration
theorem unit_iU_smul (b : Γ(X, U)) (m : Γ(M, U)) :
    ((pullbackPushforwardAdjunction (iU U hU)).unit.app M).app U (b • m)
      = ((iU U hU).app U).hom b •
        (show Γ(M' U hU M, (iU U hU) ⁻¹ᵁ U) from ((pullbackPushforwardAdjunction (iU U
          hU)).unit.app M).app U m) :=
  Scheme.Modules.Hom.app_smul _ _ _
theorem

ρ_smul

L512 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.ρ_smul
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U) (M : X.Modules)
Lean source · full declaration
theorem ρ_smul (b : Γ(X, U)) (m : Γ(M, U)) :
    ρ U hU M (b • m) = (b • (show N' U hU M from ρ U hU M m) : N' U hU M) := by
  have h2 := congrArg ((M' U hU M).presheaf.map (homOfLE (top_le_preimage_iU U hU)).op)
    (unit_iU_smul U hU M b m)
  have h3 := Scheme.Modules.map_smul (M' U hU M) (homOfLE (top_le_preimage_iU U hU)) (((iU U
    hU).app U).hom b)
    (show Γ(M' U hU M, (iU U hU) ⁻¹ᵁ U) from ((pullbackPushforwardAdjunction (iU U hU)).unit.app
      M).app U m)
  rw [iU_appLE] at h3
  exact (h2.trans h3).trans (N'_smul_def' U hU M b _).symm
def

ρlin

L524 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.ρlin
Documentation

The affine-chart section map as a linear map.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U) (M : X.Modules)
Lean source · full declaration
def ρlin : Γ(M, U) →ₗ[Γ(X, U)] N' U hU M where
  toFun m := ρ U hU M m
  map_add' x y := map_add _ x y
  map_smul' b m := ρ_smul U hU M b m
theorem

ρlin_apply

L529 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.ρlin_apply
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U) (M : X.Modules)
Lean source · statement
theorem ρlin_apply (m : Γ(M, U)) : ρlin U hU M m = ρ U hU M m
def

ρR

L585 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.ρR
Documentation

The affine-chart section map as a linear equivalence.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U) (M : X.Modules)
Lean source · statement
def ρR : Γ(M, U) ≃ₗ[Γ(X, U)] N' U hU M
theorem

ρR_apply

L591 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.ρR_apply
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U) (M : X.Modules)
Lean source · statement
theorem ρR_apply (m : Γ(M, U)) : ρR U hU M m = ρ U hU M m
abbrev

T₁

L594 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.T₁
Documentation

The scalar extension of the affine-chart section module.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U) (M : X.Modules)
Lean source · statement
abbrev T₁ : Type u
abbrev

S₁

L597 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.S₁
Documentation

The scalar-restricted coefficient module.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U) (M : X.Modules)
Lean source · statement
abbrev S₁ : ModuleCat Γ(X, U)
def

Kfwd

L601 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.Kfwd
Documentation

The additive comparison from the tensor product to scalar extension.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U) (M : X.Modules)
Lean source · full declaration
def Kfwd : letI : Algebra Γ(X, U) Γ(Y, i ⁻¹ᵁ U) := (i.app U).hom.toAlgebra
    Γ(Y, i ⁻¹ᵁ U) ⊗[Γ(X, U)] Γ(M, U) →+ T₁ i U hU M :=
  letI : Algebra Γ(X, U) Γ(Y, i ⁻¹ᵁ U) := (i.app U).hom.toAlgebra
  TensorProduct.liftAddHom
    { toFun := fun a =>
        (TensorProduct.mk Γ(X, U) (S₁ i U) (N' U hU M) (a : S₁ i U)).toAddMonoidHom.comp
          (ρlin U hU M).toAddMonoidHom
      map_zero' := by
        apply AddMonoidHom.ext; intro m
        change ((((0 : Γ(Y, i ⁻¹ᵁ U)) : S₁ i U) ⊗ₜ[Γ(X, U)] (ρlin U hU M m)) : T₁ i U hU M) = 0
        exact TensorProduct.zero_tmul _ _
      map_add' := fun a a' => by
        apply AddMonoidHom.ext; intro m
        change ((((a + a' : Γ(Y, i ⁻¹ᵁ U)) : S₁ i U)) ⊗ₜ[Γ(X, U)] (ρlin U hU M m) : T₁ i U hU M)
          = ((a : S₁ i U) ⊗ₜ[Γ(X, U)] (ρlin U hU M m) : T₁ i U hU M)
            + ((a' : S₁ i U) ⊗ₜ[Γ(X, U)] (ρlin U hU M m) : T₁ i U hU M)
        exact TensorProduct.add_tmul _ _ _ }
    (fun b a m => by
      change (((b • a : Γ(Y, i ⁻¹ᵁ U)) : S₁ i U) ⊗ₜ[Γ(X, U)] (ρlin U hU M m) : T₁ i U hU M)
        = ((a : S₁ i U) ⊗ₜ[Γ(X, U)] (ρlin U hU M (b • m)) : T₁ i U hU M)
      rw [LinearMap.map_smul]
      exact TensorProduct.smul_tmul (R := Γ(X, U)) (M := S₁ i U) (N := N' U hU M)
        b (a : S₁ i U) (ρlin U hU M m))
theorem

Kfwd_tmul

L626 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.Kfwd_tmul
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U) (M : X.Modules)
omit [IsAffineHom i] in
Lean source · full declaration
theorem Kfwd_tmul (a : Γ(Y, i ⁻¹ᵁ U)) (m : Γ(M, U)) :
    let : Algebra Γ(X, U) Γ(Y, i ⁻¹ᵁ U) := (i.app U).hom.toAlgebra
    Kfwd i U hU M (a ⊗ₜ[Γ(X, U)] m)
      = ((a : S₁ i U) ⊗ₜ[Γ(X, U)] (ρlin U hU M m) : T₁ i U hU M) := by
  let : Algebra Γ(X, U) Γ(Y, i ⁻¹ᵁ U) := (i.app U).hom.toAlgebra
  exact TensorProduct.liftAddHom_tmul _ _ a m
def

Kbwd₀

L634 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.Kbwd₀
Documentation

The bilinear inverse comparison on scalar coefficients and sections.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U) (M : X.Modules)
Lean source · full declaration
def Kbwd₀ : letI : Algebra Γ(X, U) Γ(Y, i ⁻¹ᵁ U) := (i.app U).hom.toAlgebra
    Γ(Y, i ⁻¹ᵁ U) →+ (N' U hU M →+ Γ(Y, i ⁻¹ᵁ U) ⊗[Γ(X, U)] Γ(M, U)) :=
  letI : Algebra Γ(X, U) Γ(Y, i ⁻¹ᵁ U) := (i.app U).hom.toAlgebra
  { toFun := fun a =>
      (TensorProduct.mk Γ(X, U) Γ(Y, i ⁻¹ᵁ U) Γ(M, U) a).toAddMonoidHom.comp
        ((ρR U hU M).symm : N' U hU M →ₗ[Γ(X, U)] Γ(M, U)).toAddMonoidHom
    map_zero' := by apply AddMonoidHom.ext; intro n; exact TensorProduct.zero_tmul _ _
    map_add' := fun a a' => by apply AddMonoidHom.ext; intro n; exact TensorProduct.add_tmul _ _ _ }
theorem

Kbwd₀_apply

L644 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.Kbwd₀_apply
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U) (M : X.Modules)
omit [IsAffineHom i] in
Lean source · full declaration
theorem Kbwd₀_apply (a : Γ(Y, i ⁻¹ᵁ U)) (n : N' U hU M) :
    letI : Algebra Γ(X, U) Γ(Y, i ⁻¹ᵁ U) := (i.app U).hom.toAlgebra
    Kbwd₀ i U hU M a n = a ⊗ₜ[Γ(X, U)] (ρR U hU M).symm n := rfl
def

Kbwd

L649 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.Kbwd
Documentation

The additive inverse comparison from scalar extension.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U) (M : X.Modules)
Lean source · full declaration
def Kbwd : letI : Algebra Γ(X, U) Γ(Y, i ⁻¹ᵁ U) := (i.app U).hom.toAlgebra
    T₁ i U hU M →+ Γ(Y, i ⁻¹ᵁ U) ⊗[Γ(X, U)] Γ(M, U) :=
  letI : Algebra Γ(X, U) Γ(Y, i ⁻¹ᵁ U) := (i.app U).hom.toAlgebra
  TensorProduct.liftAddHom
    (show S₁ i U →+ (N' U hU M →+ Γ(Y, i ⁻¹ᵁ U) ⊗[Γ(X, U)] Γ(M, U)) from Kbwd₀ i U hU M)
    (fun b a n => by
      change Kbwd₀ i U hU M (b • a) n = Kbwd₀ i U hU M a (b • n)
      erw [Kbwd₀_apply, Kbwd₀_apply, LinearEquiv.map_smul]
      exact TensorProduct.smul_tmul (R := Γ(X, U))
        (M := Γ(Y, i ⁻¹ᵁ U)) (N := Γ(M, U)) b a ((ρR U hU M).symm n))
theorem

Kbwd_tmul

L661 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.Kbwd_tmul
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U) (M : X.Modules)
omit [IsAffineHom i] in
Lean source · full declaration
theorem Kbwd_tmul (a : Γ(Y, i ⁻¹ᵁ U)) (n : N' U hU M) :
    letI : Algebra Γ(X, U) Γ(Y, i ⁻¹ᵁ U) := (i.app U).hom.toAlgebra
    Kbwd i U hU M ((a : S₁ i U) ⊗ₜ[Γ(X, U)] n : T₁ i U hU M) = Kbwd₀ i U hU M a n := by
  let : Algebra Γ(X, U) Γ(Y, i ⁻¹ᵁ U) := (i.app U).hom.toAlgebra
  exact TensorProduct.liftAddHom_tmul _ _ a n
def

κ

L668 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.κ
Documentation

The linear equivalence between the two scalar-extension models.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U) (M : X.Modules)
Lean source · full declaration
def κ : letI : Algebra Γ(X, U) Γ(Y, i ⁻¹ᵁ U) := (i.app U).hom.toAlgebra
    Γ(Y, i ⁻¹ᵁ U) ⊗[Γ(X, U)] Γ(M, U) ≃+ T₁ i U hU M :=
  letI : Algebra Γ(X, U) Γ(Y, i ⁻¹ᵁ U) := (i.app U).hom.toAlgebra
  { Kfwd i U hU M with
    invFun := Kbwd i U hU M
    left_inv := fun z => by
      change Kbwd i U hU M (Kfwd i U hU M z) = z
      induction z using TensorProduct.inductionOn with
      | add x y hx hy =>
        exact (congrArg (Kbwd i U hU M) (map_add (Kfwd i U hU M) x y)).trans
          ((map_add (Kbwd i U hU M) _ _).trans (congrArg₂ (· + ·) hx hy))
      | tmul a m =>
        rw [Kfwd_tmul]
        refine (Kbwd_tmul i U hU M _ _).trans ?_
        rw [Kbwd₀_apply]
        congr 1
        exact (ρR U hU M).symm_apply_apply m
    right_inv := fun t => by
      change Kfwd i U hU M (Kbwd i U hU M t) = t
      induction t using TensorProduct.inductionOn with
      | add x y hx hy =>
        exact (congrArg (Kfwd i U hU M) (map_add (Kbwd i U hU M) x y)).trans
          ((map_add (Kfwd i U hU M) _ _).trans (congrArg₂ (· + ·) hx hy))
      | tmul a n =>
        refine (congrArg (Kfwd i U hU M) (Kbwd_tmul i U hU M a n)).trans ?_
        refine (congrArg (Kfwd i U hU M) (Kbwd₀_apply i U hU M a n)).trans ?_
        refine (Kfwd_tmul i U hU M a ((ρR U hU M).symm n)).trans ?_
        congr 1
        exact (ρR U hU M).apply_symm_apply n }
theorem

κ_tmul

L699 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.κ_tmul
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U) (M : X.Modules)
omit [IsAffineHom i] in
Lean source · full declaration
theorem κ_tmul (a : Γ(Y, i ⁻¹ᵁ U)) (m : Γ(M, U)) :
    letI : Algebra Γ(X, U) Γ(Y, i ⁻¹ᵁ U) := (i.app U).hom.toAlgebra
    κ i U hU M (a ⊗ₜ[Γ(X, U)] m) = ((a : S₁ i U) ⊗ₜ[Γ(X, U)] ρ U hU M m : T₁ i U hU M) :=
  Kfwd_tmul i U hU M a m
abbrev

Q

L761 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.Q
Documentation

The module of sections after affine base change.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U) (M : X.Modules)
Lean source · statement
abbrev Q : ModuleCat (Γ(Y, i ⁻¹ᵁ U))
def

β

L766 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.β
Documentation

The affine base-change map on modules of sections.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U) (M : X.Modules)
Lean source · statement
def β : (ModuleCat.extendScalars (i.app U).hom).obj (N' U hU M) ⟶ Q i U hU M
theorem

β_tmul

L774 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.β_tmul
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U) (M : X.Modules)
omit [IsAffineHom i] in
Lean source · full declaration
theorem β_tmul (x : Γ(Y, i ⁻¹ᵁ U)) (n : N' U hU M) :
    (β i U hU M).hom ((x : S₁ i U) ⊗ₜ[Γ(X, U)] n : T₁ i U hU M) = x • (show Q i U hU M from ηφ i U
      hU M n) := by
  unfold β
  rw [Adjunction.homEquiv_counit]
  rfl
theorem

Q_smul_def

L782 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.Q_smul_def
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U) (M : X.Modules)
omit [IsAffineHom i] in
Lean source · full declaration
theorem Q_smul_def (x : Γ(Y, i ⁻¹ᵁ U)) (q : Q i U hU M) :
    x • q = ((Scheme.ΓSpecIso (Γ(Y, i ⁻¹ᵁ U))).inv.hom x) •
      (show Γ((Scheme.Modules.pullback (Spec.map (i.app U))).obj (M' U hU M), ⊤) from q) := by
  have h1 : x • q = (((Spec Γ(Y, i ⁻¹ᵁ U)).presheaf.map (homOfLE (le_top : (⊤ : (Spec Γ(Y, i ⁻¹ᵁ
    U)).Opens) ≤ ⊤)).op).hom
      ((StructureSheaf.globalSectionsIso (Γ(Y, i ⁻¹ᵁ U))).hom.hom x)) •
      (show Γ((Scheme.Modules.pullback (Spec.map (i.app U))).obj (M' U hU M), ⊤) from q) := rfl
  rw [h1]
  congr 1
theorem

σ_smul

L792 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.σ_smul
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U) (M : X.Modules)
Lean source · statement
theorem σ_smul (t : Γ(Spec Γ(Y, i ⁻¹ᵁ U), ⊤)) (q : Γ((Scheme.Modules.pullback (Spec.map (i.app
  U))).obj (M' U hU M), ⊤)) :
    (σ i U hU M).hom.app ⊤ (t • q) = t • (σ i U hU M).hom.app ⊤ q
theorem

θ_smul

L797 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.θ_smul
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U) (M : X.Modules)
Lean source · statement
theorem θ_smul (s : Γ(Y, i ⁻¹ᵁ U)) (y : Γ(MY i M, i ⁻¹ᵁ U)) :
    θ i U hU M (s • y) =
      ((j i U hU).appLE (i ⁻¹ᵁ U) ⊤ (top_le_preimage_j i U hU)).hom s • θ i U hU M y
theorem

scalar_key

L813 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.scalar_key
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U) (M : X.Modules)
Lean source · statement
theorem scalar_key (a : Γ(Y, i ⁻¹ᵁ U)) :
    ((j i U hU).appLE (i ⁻¹ᵁ U) ⊤ (top_le_preimage_j i U hU)).hom a
      = (Scheme.ΓSpecIso Γ(Y, i ⁻¹ᵁ U)).inv.hom a
abbrev

P

L831 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.P
Documentation

Sections of the pullback over the inverse-image open.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U) (M : X.Modules)
Lean source · statement
abbrev P : Type u
abbrev

instRP

L834 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.instRP
Documentation

The original-open scalar action on pullback sections.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U) (M : X.Modules)
Lean source · statement
abbrev instRP : Module Γ(X, U) (P i U M)
theorem

isScalarTower_RSP

L837 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.isScalarTower_RSP
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U) (M : X.Modules)
omit [IsAffineHom i] in
Lean source · full declaration
theorem isScalarTower_RSP : letI : Algebra Γ(X, U) Γ(Y, i ⁻¹ᵁ U) := (i.app U).hom.toAlgebra
    letI := instRP i U M; IsScalarTower Γ(X, U) Γ(Y, i ⁻¹ᵁ U) (P i U M) :=
  letI : Algebra Γ(X, U) Γ(Y, i ⁻¹ᵁ U) := (i.app U).hom.toAlgebra
  letI := instRP i U M
  IsScalarTower.of_algebraMap_smul fun _ _ => rfl
theorem

unit_smul

L844 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.unit_smul
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U) (M : X.Modules)
omit [IsAffineHom i] in
Lean source · full declaration
theorem unit_smul (b : Γ(X, U)) (m : Γ(M, U)) :
    ((pullbackPushforwardAdjunction i).unit.app M).app U (b • m)
      = (i.app U).hom b • (show P i U M from ((pullbackPushforwardAdjunction i).unit.app M).app U
        m) :=
  Scheme.Modules.Hom.app_smul _ _ _
def

ηR

L851 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.ηR
Documentation

The adjunction unit on sections, with scalars restricted.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U) (M : X.Modules)
Lean source · full declaration
def ηR : letI := instRP i U M
    Γ(M, U) →ₗ[Γ(X, U)] P i U M :=
  letI := instRP i U M
  { toFun := fun m => η i U M m
    map_add' := fun x y => map_add _ x y
    map_smul' := fun r m => by
      change η i U M (r • m) = ((i.app U).hom r) • η i U M m
      exact unit_smul i U M r m }
theorem

ηR_apply

L861 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.ηR_apply
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U) (M : X.Modules)
omit [IsAffineHom i] in
Lean source · full declaration
theorem ηR_apply (m : Γ(M, U)) : letI := instRP i U M
    ηR i U M m = η i U M m := rfl
def

e₀

L865 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.e₀
Documentation

The linear map induced by the adjunction unit on sections.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U) (M : X.Modules)
Lean source · full declaration
def e₀ : letI : Algebra Γ(X, U) Γ(Y, i ⁻¹ᵁ U) := (i.app U).hom.toAlgebra
    Γ(Y, i ⁻¹ᵁ U) ⊗[Γ(X, U)] Γ(M, U) →ₗ[Γ(Y, i ⁻¹ᵁ U)] P i U M :=
  letI : Algebra Γ(X, U) Γ(Y, i ⁻¹ᵁ U) := (i.app U).hom.toAlgebra
  letI := instRP i U M
  haveI := isScalarTower_RSP i U M
  LinearMap.liftBaseChange Γ(Y, i ⁻¹ᵁ U) (ηR i U M)
theorem

e₀_tmul

L873 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.e₀_tmul
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U) (M : X.Modules)
omit [IsAffineHom i] in
Lean source · full declaration
theorem e₀_tmul (a : Γ(Y, i ⁻¹ᵁ U)) (m : Γ(M, U)) :
    letI : Algebra Γ(X, U) Γ(Y, i ⁻¹ᵁ U) := (i.app U).hom.toAlgebra
    e₀ i U M (a ⊗ₜ[Γ(X, U)] m) = a • η i U M m :=
  let : Algebra Γ(X, U) Γ(Y, i ⁻¹ᵁ U) := (i.app U).hom.toAlgebra
  letI := instRP i U M
  haveI := isScalarTower_RSP i U M
  LinearMap.liftBaseChange_tmul Γ(Y, i ⁻¹ᵁ U) (ηR i U M) a m
theorem

θ_e₀

L881 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.θ_e₀
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U) (M : X.Modules)
Lean source · full declaration
theorem θ_e₀ (z : letI : Algebra Γ(X, U) Γ(Y, i ⁻¹ᵁ U) := (i.app U).hom.toAlgebra
      Γ(Y, i ⁻¹ᵁ U) ⊗[Γ(X, U)] Γ(M, U)) :
    letI : Algebra Γ(X, U) Γ(Y, i ⁻¹ᵁ U) := (i.app U).hom.toAlgebra
    θ i U hU M (e₀ i U M z) = (σ i U hU M).hom.app ⊤ ((β i U hU M).hom (κ i U hU M z)) := by
  let : Algebra Γ(X, U) Γ(Y, i ⁻¹ᵁ U) := (i.app U).hom.toAlgebra
  induction z using TensorProduct.inductionOn with
  | add x y hx hy =>
    simp only [map_add, hx, hy]
    first | rfl | exact (map_add _ _ _).symm
  | tmul a m =>
    rw [e₀_tmul, κ_tmul]
    have hβ := β_tmul i U hU M a (ρ U hU M m)
    have hQ := Q_smul_def i U hU M a (ηφ i U hU M (ρ U hU M m))
    have hσ := σ_smul i U hU M ((Scheme.ΓSpecIso Γ(Y, i ⁻¹ᵁ U)).inv.hom a)
      (ηφ i U hU M (ρ U hU M m))
    have hright := (congrArg (fun q : Q i U hU M => (σ i U hU M).hom.app ⊤ q)
      (hβ.trans hQ)).trans hσ
    have hchase := congrArg
      (fun n : Γ((Scheme.Modules.pullback (j i U hU)).obj (MY i M), ⊤) =>
        (Scheme.ΓSpecIso Γ(Y, i ⁻¹ᵁ U)).inv.hom a • n) (chase i U hU M m)
    have hleft := (θ_smul i U hU M a (η i U M m)).trans
      (congrArg (fun s : Γ(Spec Γ(Y, i ⁻¹ᵁ U), ⊤) => s • θ i U hU M (η i U M m))
        (scalar_key i U hU a))
    exact hleft.trans (hright.trans hchase).symm
theorem

bijective_e₀

L907 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.bijective_e₀
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U) (M : X.Modules)
include hU in
Lean source · full declaration
theorem bijective_e₀
    (htriv : ∀ x : X, ∃ (V : X.Opens), x ∈ V ∧
      Nonempty ((Scheme.Modules.pullback V.ι).obj M ≅ SheafOfModules.unit V.toScheme.ringCatSheaf))
    (hB2c : ∀ (N : (Spec Γ(X, U)).Modules),
      (∀ y : Spec Γ(X, U), ∃ (V : (Spec Γ(X, U)).Opens), y ∈ V ∧
        Nonempty ((Scheme.Modules.pullback V.ι).obj N ≅ SheafOfModules.unit
          V.toScheme.ringCatSheaf)) →
      IsIso N.fromTildeΓ)
    (hC1 : ∀ (N : (Spec Γ(X, U)).Modules), IsIso N.fromTildeΓ →
      IsIso (((ModuleCat.extendRestrictScalarsAdj (i.app U).hom).homEquiv
        ((moduleSpecΓFunctor (R := Γ(X, U))).obj N)
        ((moduleSpecΓFunctor (R := Γ(Y, i ⁻¹ᵁ U))).obj ((Scheme.Modules.pullback (Spec.map (i.app
          U))).obj N))).symm
      ((moduleSpecΓFunctor (R := Γ(X, U))).map
          ((Scheme.Modules.pullbackPushforwardAdjunction (Spec.map (i.app U))).unit.app N) ≫
        (Scheme.Modules.pushforwardSpecCompΓIso (i.app U)).hom.app
          ((Scheme.Modules.pullback (Spec.map (i.app U))).obj N)))) :
    letI : Algebra Γ(X, U) Γ(Y, i ⁻¹ᵁ U) := (i.app U).hom.toAlgebra
    Function.Bijective (e₀ i U M) := by
  let : Algebra Γ(X, U) Γ(Y, i ⁻¹ᵁ U) := (i.app U).hom.toAlgebra
  have hM' : IsIso (M' U hU M).fromTildeΓ := hB2c _ (locallyTrivial_pullback (iU U hU) M htriv)
  have hβ : IsIso (β i U hU M) := hC1 _ hM'
  have bβ : Function.Bijective (β i U hU M).hom := by
    have := ConcreteCategory.bijective_of_isIso (β i U hU M); exact this
  have bσ : Function.Bijective ((σ i U hU M).hom.app ⊤) := by
    rw [← ConcreteCategory.isIso_iff_bijective]; infer_instance
  have bθ := bijective_θ i U hU M
  have bκ : Function.Bijective (κ i U hU M) := (κ i U hU M).bijective
  have hcomp : Function.Bijective (fun z => θ i U hU M (e₀ i U M z)) := by
    have heq : (fun z => θ i U hU M (e₀ i U M z))
        = (fun z => (σ i U hU M).hom.app ⊤ ((β i U hU M).hom (κ i U hU M z))) := funext (θ_e₀ i U
          hU M)
    rw [heq]
    exact bσ.comp (bβ.comp bκ)
  constructor
  · exact Function.Injective.of_comp hcomp.1
  · intro p
    obtain ⟨z, hz⟩ := hcomp.2 (θ i U hU M p)
    exact ⟨z, bθ.1 hz⟩
theorem

main

L948 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.main
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ClosedImmersionSectionEquiv
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace SectionsCI
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (i : Y ⟶ X) [IsAffineHom i]
variable (U : X.Opens) (hU : IsAffineOpen U) (M : X.Modules)
include hU in
Lean source · full declaration
theorem main
    (htriv : ∀ x : X, ∃ (V : X.Opens), x ∈ V ∧
      Nonempty ((Scheme.Modules.pullback V.ι).obj M ≅ SheafOfModules.unit V.toScheme.ringCatSheaf))
    (hB2c : ∀ (N : (Spec Γ(X, U)).Modules),
      (∀ y : Spec Γ(X, U), ∃ (V : (Spec Γ(X, U)).Opens), y ∈ V ∧
        Nonempty ((Scheme.Modules.pullback V.ι).obj N ≅ SheafOfModules.unit
          V.toScheme.ringCatSheaf)) →
      IsIso N.fromTildeΓ)
    (hC1 : ∀ (N : (Spec Γ(X, U)).Modules), IsIso N.fromTildeΓ →
      IsIso (((ModuleCat.extendRestrictScalarsAdj (i.app U).hom).homEquiv
        ((moduleSpecΓFunctor (R := Γ(X, U))).obj N)
        ((moduleSpecΓFunctor (R := Γ(Y, i ⁻¹ᵁ U))).obj ((Scheme.Modules.pullback (Spec.map (i.app
          U))).obj N))).symm
      ((moduleSpecΓFunctor (R := Γ(X, U))).map
          ((Scheme.Modules.pullbackPushforwardAdjunction (Spec.map (i.app U))).unit.app N) ≫
        (Scheme.Modules.pushforwardSpecCompΓIso (i.app U)).hom.app
          ((Scheme.Modules.pullback (Spec.map (i.app U))).obj N)))) :
    letI : Algebra Γ(X, U) Γ(Y, i ⁻¹ᵁ U) := (i.app U).hom.toAlgebra
    ∃ e : Γ(Y, i ⁻¹ᵁ U) ⊗[Γ(X, U)] Γ(M, U) ≃ₗ[Γ(Y, i ⁻¹ᵁ U)] Γ((Scheme.Modules.pullback i).obj M, i
      ⁻¹ᵁ U),
      ∀ m : Γ(M, U), e (1 ⊗ₜ m) = (((Scheme.Modules.pullbackPushforwardAdjunction i).unit.app
        M).app U).hom m := by
  let : Algebra Γ(X, U) Γ(Y, i ⁻¹ᵁ U) := (i.app U).hom.toAlgebra
  refine ⟨LinearEquiv.ofBijective (e₀ i U M) (bijective_e₀ i U hU M htriv hB2c hC1), fun m => ?_⟩
  rw [LinearEquiv.ofBijective_apply, e₀_tmul, one_smul]
  rfl
theorem

exists_linearEquiv_sections_pullback_of_isClosedImmersion_of_locallyTrivial

L995 ↗
AlgebraicGeometry.Scheme.Modules.exists_linearEquiv_sections_pullback_of_isClosedImmersion_of_locallyTrivial
Source context 5 commands

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

section ProofImplementation
open AlgebraicCurves.Geometry.Sheaves.Proofs
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Modules
universe u
Lean source · full declaration
theorem exists_linearEquiv_sections_pullback_of_isClosedImmersion_of_locallyTrivial
    {X Y : Scheme.{u}} (i : Y ⟶ X) [IsClosedImmersion i] (M : X.Modules)
    (htriv : ∀ x : X, ∃ V : X.Opens, x ∈ V ∧
      Nonempty ((Scheme.Modules.pullback V.ι).obj M ≅ SheafOfModules.unit V.toScheme.ringCatSheaf))
    (U : X.Opens) (hU : IsAffineOpen U) :
    letI : Algebra Γ(X, U) Γ(Y, i ⁻¹ᵁ U) := (i.app U).hom.toAlgebra
    ∃ e : Γ(Y, i ⁻¹ᵁ U) ⊗[Γ(X, U)] Γ(M, U) ≃ₗ[Γ(Y, i ⁻¹ᵁ U)] Γ((Scheme.Modules.pullback i).obj M, i
      ⁻¹ᵁ U),
      ∀ m : Γ(M, U), e (1 ⊗ₜ m) = (((Scheme.Modules.pullbackPushforwardAdjunction i).unit.app
        M).app U).hom m :=
  ClosedImmersionSectionEquiv.AlgebraicGeometry.Scheme.Modules.SectionsCI.main i U hU M htriv
    (fun N h => AlgebraicGeometry.Scheme.Modules.isIso_fromTildeGamma_of_locallyTrivial N h)
    (fun N h => AlgebraicGeometry.Scheme.Modules.isIso_baseChange_sections_of_isIso_fromTildeGamma
      (i.app U) N h)

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