NYLL
Module

Scheme_TwoAffineOpenCover_exists_isPullback_snd_specMap_algebraOfHom.lean

Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_TwoAffineOpenCover_exists_isPullback_snd_specMap_algebraOfHom
7 declarations indexed from sourceView source ↗

Module documentation

Cartesian chart pullbacks along an affine base open

An affine open of the base identifies its chart-ring spectrum with the open and gives compatible Cartesian presentations of the curve pullback and chart modules.

Imports8
Imported by13

Declarations

def

pushforwardIsoEquivalence

L57 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_isPullback_snd_specMap_algebraOfHom.AlgebraicGeometry.Scheme.Modules.pushforwardIsoEquivalence
Documentation

Pushforward along the two directions of a scheme isomorphism gives inverse equivalences of module categories.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isPullback_snd_specMap_algebraOfHom
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section iso
variable {Y Y' : Scheme.{u}} (e : Y ≅ Y')
Lean source · statement
def pushforwardIsoEquivalence : Y.Modules ≌ Y'.Modules
def

pullbackIsoPushforwardInv

L65 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_isPullback_snd_specMap_algebraOfHom.AlgebraicGeometry.Scheme.Modules.pullbackIsoPushforwardInv
Documentation

Pullback along the isomorphism identifies with pushforward along its inverse, by uniqueness of left adjoints.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isPullback_snd_specMap_algebraOfHom
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section iso
variable {Y Y' : Scheme.{u}} (e : Y ≅ Y')
Lean source · statement
def pullbackIsoPushforwardInv : Scheme.Modules.pullback e.hom ≅ pushforward e.inv
theorem

isLocallyFreeOfRank_pushforward_of_forall_exists_isPullback_aux

L71 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_isPullback_snd_specMap_algebraOfHom.AlgebraicGeometry.Scheme.Modules.isLocallyFreeOfRank_pushforward_of_forall_exists_isPullback_aux
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isPullback_snd_specMap_algebraOfHom
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
Lean source · statement
theorem isLocallyFreeOfRank_pushforward_of_forall_exists_isPullback_aux
    {X T : Scheme.{u}} (π : X ⟶ T) (F : X.Modules) (n : ℕ)
    (h : ∀ y : T, ∃ (W : T.Opens), y ∈ W ∧ ∃ (W' X' : Scheme.{u}) (e : W' ≅ W.toScheme) (π' : X'
        ⟶ W')
      (g' : X' ⟶ X), IsPullback g' π' π (e.hom ≫ W.ι) ∧
        IsLocallyFreeOfRank n ((pushforward π').obj ((Scheme.Modules.pullback g').obj F))) :
    IsLocallyFreeOfRank n ((pushforward π).obj F)
theorem

exists_iso_pullback_of_isPullback_aux

L114 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_isPullback_snd_specMap_algebraOfHom.AlgebraicGeometry.Scheme.Modules.exists_iso_pullback_of_isPullback_aux
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isPullback_snd_specMap_algebraOfHom
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
Lean source · statement
theorem exists_iso_pullback_of_isPullback_aux
    {X T X' W' Z : Scheme.{u}} (π : X ⟶ T) (π' : X' ⟶ W') (g' : X' ⟶ X) (j : W' ⟶ T)
    (hcart : IsPullback g' π' π j) (s : Z ⟶ W') :
    ∃ φ : Limits.pullback π (s ≫ j) ≅ Limits.pullback π' s,
      φ.hom ≫ Limits.pullback.snd π' s = Limits.pullback.snd π (s ≫ j) ∧
      φ.hom ≫ Limits.pullback.fst π' s ≫ g' = Limits.pullback.fst π (s ≫ j) ∧
      ∀ G : X.Modules, Nonempty ((Scheme.Modules.pullback (Limits.pullback.fst π (s ≫ j))).obj G ≅
        (Scheme.Modules.pullback φ.hom).obj ((Scheme.Modules.pullback (Limits.pullback.fst π'
            s)).obj
          ((Scheme.Modules.pullback g').obj G)))
theorem

exists_isPullback_snd_specMap_algebraOfHom_aux

L148 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_isPullback_snd_specMap_algebraOfHom.AlgebraicGeometry.Scheme.TwoAffineOpenCover.exists_isPullback_snd_specMap_algebraOfHom_aux
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isPullback_snd_specMap_algebraOfHom
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
Lean source · full declaration
theorem exists_isPullback_snd_specMap_algebraOfHom_aux
    {R : Type u} [CommRing R] {C T : Scheme.{u}} (c : C ⟶ Spec (.of R)) (t : T ⟶ Spec (.of R))
    (W : T.Opens) (hW : IsAffineOpen W) :
    letI := algebraOfHom t W
    ∃ g' : Limits.pullback c (specMap R Γ(T, W)) ⟶ Limits.pullback c t,
      IsPullback g' (Limits.pullback.snd c (specMap R Γ(T, W))) (Limits.pullback.snd c t)
          hW.fromSpec ∧
        g' ≫ Limits.pullback.fst c t = Limits.pullback.fst c (specMap R Γ(T, W)) := by
  let := algebraOfHom t W
  have key : hW.fromSpec ≫ t = specMap R Γ(T, W) := by
    have h := IsAffineOpen.SpecMap_appLE_fromSpec t (isAffineOpen_top _) hW (le_top (a := W))
    rw [IsAffineOpen.fromSpec_top, Scheme.isoSpec_Spec_inv, ← Spec.map_comp] at h
    change _ = Spec.map (CommRingCat.ofHom ((Scheme.ΓSpecIso (.of R)).inv ≫ t.appLE ⊤ W le_top).hom)
    rw [CommRingCat.ofHom_hom]
    exact h.symm
  let e₁ : Limits.pullback (Limits.pullback.snd c t) hW.fromSpec ≅ Limits.pullback c (specMap R
      Γ(T, W)) :=
    pullbackLeftPullbackSndIso c t hW.fromSpec ≪≫ Limits.pullback.congrHom rfl key
  have h1 : IsPullback (Limits.pullback.fst (Limits.pullback.snd c t) hW.fromSpec)
      (Limits.pullback.snd (Limits.pullback.snd c t) hW.fromSpec) (Limits.pullback.snd c t)
          hW.fromSpec :=
    IsPullback.of_hasPullback _ _
  refine ⟨e₁.inv ≫ Limits.pullback.fst (Limits.pullback.snd c t) hW.fromSpec, ?_, ?_⟩
  swap
  · rw [Category.assoc, Iso.inv_comp_eq]
    simp only [e₁, Iso.trans_hom, Category.assoc, Limits.pullback.congrHom_hom]
    delta CategoryTheory.Limits.pullback.map
    rw [Limits.pullback.lift_fst, Category.comp_id, pullbackLeftPullbackSndIso_hom_fst]
  refine h1.of_iso e₁ (Iso.refl _) (Iso.refl _) (Iso.refl _) (by simp) ?_ (by simp) (by simp)
  simp only [e₁, Iso.trans_hom, Iso.refl_hom, Category.comp_id, Category.assoc,
      Limits.pullback.congrHom_hom]
  delta CategoryTheory.Limits.pullback.map
  rw [Limits.pullback.lift_snd, Category.comp_id, pullbackLeftPullbackSndIso_hom_snd]
theorem

finiteType_algebraOfHom_aux

L182 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_isPullback_snd_specMap_algebraOfHom.AlgebraicGeometry.Scheme.TwoAffineOpenCover.finiteType_algebraOfHom_aux
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isPullback_snd_specMap_algebraOfHom
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
Lean source · full declaration
theorem finiteType_algebraOfHom_aux {R : Type u} [CommRing R] {T : Scheme.{u}} (t : T ⟶ Spec
    (.of R))
    [LocallyOfFiniteType t] (W : T.Opens) (hW : IsAffineOpen W) :
    letI := algebraOfHom t W
    Algebra.FiniteType R Γ(T, W) := by
  let := algebraOfHom t W
  have h : (t.appLE ⊤ W le_top).hom.FiniteType :=
    t.finiteType_appLE (isAffineOpen_top _) hW le_top
  have h' : (Scheme.ΓSpecIso (.of R)).inv.hom.FiniteType :=
    RingHom.FiniteType.of_surjective _ (Scheme.ΓSpecIso (.of
        R)).symm.commRingCatIsoToRingEquiv.surjective
  rw [← RingHom.finiteType_algebraMap]
  exact h.comp h'
theorem

exists_isPullback_snd_specMap_algebraOfHom

L204 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.exists_isPullback_snd_specMap_algebraOfHom
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isPullback_snd_specMap_algebraOfHom
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
with_weak_namespace _root_.AlgebraicCurves.Geometry.Schemes.Proofs
with_weak_namespace Scheme_TwoAffineOpenCover_exists_isPullback_snd_specMap_algebraOfHom
with_weak_namespace AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover TwoAffineOpenCover in
with_weak_namespace _root_.AlgebraicCurves.Geometry.Schemes.Proofs
with_weak_namespace Scheme_TwoAffineOpenCover_exists_isPullback_snd_specMap_algebraOfHom
Lean source · full declaration
theorem
    _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.exists_isPullback_snd_specMap_algebraOfHom
    {R : Type u} [CommRing R] {C T : Scheme.{u}} (c : C ⟶ Spec (.of R)) (t : T ⟶ Spec (.of R))
    (W : T.Opens) (hW : IsAffineOpen W) :
    letI := Scheme.TwoAffineOpenCover.algebraOfHom t W
    ∃ g' : Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R Γ(T, W)) ⟶ Limits.pullback c t,
      IsPullback g' (Limits.pullback.snd c (Scheme.TwoAffineOpenCover.specMap R Γ(T, W)))
          (Limits.pullback.snd c t)
        hW.fromSpec ∧
      g' ≫ Limits.pullback.fst c t = Limits.pullback.fst c (Scheme.TwoAffineOpenCover.specMap R
          Γ(T, W)) :=
  exists_isPullback_snd_specMap_algebraOfHom_aux c t W hW

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