NYLL
Module

Scheme_TwoAffineOpenCover_subsingleton_H1_sectionsOf_of_forall_field.lean

Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_TwoAffineOpenCover_subsingleton_H1_sectionsOf_of_forall_field
3 declarations indexed from sourceView source ↗

Module documentation

Scheme Two Affine Open Cover subsingleton H1 sections Of of forall field

Imports4
Imported by2

Declarations

theorem

subsingleton_of_forall_maximal

L48 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_subsingleton_H1_sectionsOf_of_forall_field.AlgebraicGeometry.Scheme.TwoAffineOpenCover.H1Fibre.subsingleton_of_forall_maximal
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_subsingleton_H1_sectionsOf_of_forall_field
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace H1Fibre
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TensorProduct
Lean source · statement
theorem subsingleton_of_forall_maximal {A : Type u} [CommRing A] (M : Type v) [AddCommGroup M]
  [Module A M]
    [Module.Finite A M]
    (h : ∀ (m : Ideal A) [m.IsMaximal], Subsingleton ((A ⧸ m) ⊗[A] M)) : Subsingleton M
theorem

main

L76 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_subsingleton_H1_sectionsOf_of_forall_field.AlgebraicGeometry.Scheme.TwoAffineOpenCover.H1Fibre.main
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_subsingleton_H1_sectionsOf_of_forall_field
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace H1Fibre
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TensorProduct
Lean source · statement
theorem main {A : Type u} [CommRing A] {X : Scheme.{u}} (π : X ⟶ Spec (.of A))
    (𝒱 : X.TwoAffineOpenCover) (F : X.Modules)
    (htriv : ∀ x : X, ∃ (V : X.Opens), x ∈ V ∧
      Nonempty ((Scheme.Modules.pullback V.ι).obj F ≅ SheafOfModules.unit V.toScheme.ringCatSheaf))
    (hfin : Module.Finite A (𝒱.sectionsOf π F).H1)
    (hfib : ∀ (K : Type u) [Field K] [Algebra A K],
      Subsingleton ((𝒱.pullback π K).sectionsOf (Limits.pullback.snd π
        (Scheme.TwoAffineOpenCover.specMap A K))
        ((Scheme.Modules.pullback (Limits.pullback.fst π (Scheme.TwoAffineOpenCover.specMap A
          K))).obj F)).H1) :
    Subsingleton (𝒱.sectionsOf π F).H1
theorem

subsingleton_H1_sectionsOf_of_forall_field

L98 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.subsingleton_H1_sectionsOf_of_forall_field
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_subsingleton_H1_sectionsOf_of_forall_field
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TensorProduct
Lean source · statement
theorem
  _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.subsingleton_H1_sectionsOf_of_forall_field
    {A : Type u} [CommRing A] {X : Scheme.{u}} (π : X ⟶ Spec (.of A))
    (𝒱 : X.TwoAffineOpenCover) (F : X.Modules)
    (htriv : ∀ x : X, ∃ (V : X.Opens), x ∈ V ∧
      Nonempty ((Scheme.Modules.pullback V.ι).obj F ≅ SheafOfModules.unit V.toScheme.ringCatSheaf))
    (hfin : Module.Finite A (𝒱.sectionsOf π F).H1)
    (hfib : ∀ (K : Type u) [Field K] [Algebra A K],
      Subsingleton ((𝒱.pullback π K).sectionsOf (Limits.pullback.snd π
        (Scheme.TwoAffineOpenCover.specMap A K))
        ((Scheme.Modules.pullback (Limits.pullback.fst π (Scheme.TwoAffineOpenCover.specMap A
          K))).obj F)).H1) :
    Subsingleton (𝒱.sectionsOf π F).H1

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