NYLL
Module

ProjSpaceCech_GradedModule_nonempty_HEquiv_pi.lean

Nyll.SchemeTheory.Cohomology.Cech.ProjSpaceCech_GradedModule_nonempty_HEquiv_pi
24 declarations indexed from sourceView source ↗

Module documentation

Cech cohomology of a finite product of graded modules is the product of their cohomologies.

Imports3
Imported by3

Declarations

def

piComm

L44 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_pi.ProjSpaceCech.GradedModule.piComm
Documentation

The linear equivalence exchanging the two indices of a dependent product of modules.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_pi
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section PiHelpers
variable {R : Type u} [CommRing R]
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · full declaration
def GradedModule.piComm {α : Type*} {β : Type*} (M : α → β → Type*)
    [∀ a b, AddCommMonoid (M a b)] [∀ a b, Module R (M a b)] :
    (∀ a, ∀ b, M a b) ≃ₗ[R] (∀ b, ∀ a, M a b) where
  toFun f b a := f a b
  invFun g a b := g b a
  map_add' _ _ := rfl
  map_smul' _ _ := rfl
  left_inv _ := rfl
  right_inv _ := rfl
theorem

piComm_apply

L55 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_pi.ProjSpaceCech.GradedModule.piComm_apply
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_pi
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section PiHelpers
variable {R : Type u} [CommRing R]
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · statement
theorem GradedModule.piComm_apply {α : Type*} {β : Type*} (M : α → β → Type*)
    [∀ a b, AddCommMonoid (M a b)] [∀ a b, Module R (M a b)]
    (f : ∀ a, ∀ b, M a b) (b : β) (a : α) :
    GradedModule.piComm (R := R) M f b a = f a b
def

piSubmodEquiv

L63 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_pi.ProjSpaceCech.GradedModule.piSubmodEquiv
Documentation

The equivalence between the product submodule and the product of its component submodules.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_pi
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section PiHelpers
variable {R : Type u} [CommRing R]
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · full declaration
def GradedModule.piSubmodEquiv {ι : Type*} {M : ι → Type*}
    [∀ k, AddCommMonoid (M k)] [∀ k, Module R (M k)] (p : ∀ k, Submodule R (M k)) :
    ↥(Submodule.pi Set.univ p) ≃ₗ[R] (∀ k, ↥(p k)) where
  toFun f k := ⟨f.1 k, f.2 k (Set.mem_univ k)⟩
  invFun g := ⟨fun k => (g k).1, fun k _ => (g k).2⟩
  map_add' _ _ := rfl
  map_smul' _ _ := rfl
  left_inv _ := rfl
  right_inv _ := rfl
theorem

piSubmodEquiv_apply_coe

L74 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_pi.ProjSpaceCech.GradedModule.piSubmodEquiv_apply_coe
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_pi
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section PiHelpers
variable {R : Type u} [CommRing R]
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · statement
theorem GradedModule.piSubmodEquiv_apply_coe {ι : Type*} {M : ι → Type*}
    [∀ k, AddCommMonoid (M k)] [∀ k, Module R (M k)] (p : ∀ k, Submodule R (M k))
    (f : ↥(Submodule.pi Set.univ p)) (k : ι) :
    ((GradedModule.piSubmodEquiv (R := R) p f k : M k)) = (f : ∀ k, M k) k
theorem

pi_monMul_apply

L88 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_pi.ProjSpaceCech.GradedModule.pi_monMul_apply
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_pi
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section PiEquiv
variable {R : Type u} [CommRing R] {n : ℕ}
variable {ι : Type} [Fintype ι] (D : ι → GradedModule R n)
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · statement
theorem GradedModule.pi_monMul_apply (a : Fin (n + 1) → ℕ)
    (m : ∀ k, (D k).M) (k : ι) :
    GradedModule.monMul (GradedModule.pi D) a m k = GradedModule.monMul (D k) a (m k)
def

secPiProj

L111 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_pi.ProjSpaceCech.GradedModule.secPiProj
Documentation

The projection from fraction sections of a product graded module to one component.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_pi
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section PiEquiv
variable {R : Type u} [CommRing R] {n : ℕ}
variable {ι : Type} [Fintype ι] (D : ι → GradedModule R n)
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · full declaration
def GradedModule.secPiProj (I : Finset (Fin (n + 1))) (k : ι) :
    GradedModule.sec (GradedModule.pi D) I →ₗ[R] GradedModule.sec (D k) I where
  toFun := Quotient.map
    (fun x => ⟨x.denExp, x.hden, x.num k, x.hnum k (Set.mem_univ k)⟩)
    (fun _ _ ⟨c, hc, heq⟩ => ⟨c, hc, by
      have h1 := congrFun heq k
      erw [GradedModule.pi_monMul_apply, GradedModule.pi_monMul_apply] at h1
      exact h1⟩)
  map_add' := by
    rintro ⟨x⟩ ⟨y⟩
    refine (GradedModule.sec_mk_eq _ I).mpr ⟨0, fun _ _ => rfl, ?_⟩
    have hnum : ((GradedModule.monMul (GradedModule.pi D) y.denExp) x.num
            + (GradedModule.monMul (GradedModule.pi D) x.denExp) y.num) k
          = (GradedModule.monMul (D k) y.denExp) (x.num k)
            + (GradedModule.monMul (D k) x.denExp) (y.num k) := by
      change (_ : (D k).M) + _ = _
      erw [GradedModule.pi_monMul_apply, GradedModule.pi_monMul_apply]
    simp only [zero_add, hnum, map_add]
  map_smul' := by
    rintro r ⟨x⟩
    refine (GradedModule.sec_mk_eq _ I).mpr ⟨0, fun _ _ => rfl, ?_⟩
    have hnum : (r • x.num) k = r • (x.num k : (D k).M) := rfl
    simp only [zero_add, hnum, map_smul, RingHom.id_apply]
def

secPiFwd

L137 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_pi.ProjSpaceCech.GradedModule.secPiFwd
Documentation

The linear map taking a product graded module fraction to its component fractions.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_pi
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section PiEquiv
variable {R : Type u} [CommRing R] {n : ℕ}
variable {ι : Type} [Fintype ι] (D : ι → GradedModule R n)
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · statement
def GradedModule.secPiFwd (I : Finset (Fin (n + 1))) :
    GradedModule.sec (GradedModule.pi D) I
      →ₗ[R] (∀ k, GradedModule.sec (D k) I)
theorem

secPiFwd_incl

L143 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_pi.ProjSpaceCech.GradedModule.secPiFwd_incl
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_pi
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section PiEquiv
variable {R : Type u} [CommRing R] {n : ℕ}
variable {ι : Type} [Fintype ι] (D : ι → GradedModule R n)
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · full declaration
theorem GradedModule.secPiFwd_incl {I J : Finset (Fin (n + 1))} (hIJ : I ⊆ J) :
    (LinearMap.pi (fun k => (GradedModule.secIncl (D k) hIJ).comp (LinearMap.proj k))).comp
        (GradedModule.secPiFwd D I)
      = (GradedModule.secPiFwd D J).comp
          (GradedModule.secIncl (GradedModule.pi D) hIJ) := by
  refine LinearMap.ext fun z => funext fun k => ?_
  obtain ⟨x⟩ := z; rfl
theorem

secPiFwd_injective

L152 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_pi.ProjSpaceCech.GradedModule.secPiFwd_injective
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_pi
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section PiEquiv
variable {R : Type u} [CommRing R] {n : ℕ}
variable {ι : Type} [Fintype ι] (D : ι → GradedModule R n)
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · statement
theorem GradedModule.secPiFwd_injective (I : Finset (Fin (n + 1))) :
    Function.Injective (GradedModule.secPiFwd D I)
theorem

secPiFwd_surjective

L180 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_pi.ProjSpaceCech.GradedModule.secPiFwd_surjective
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_pi
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section PiEquiv
variable {R : Type u} [CommRing R] {n : ℕ}
variable {ι : Type} [Fintype ι] (D : ι → GradedModule R n)
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · statement
theorem GradedModule.secPiFwd_surjective (I : Finset (Fin (n + 1))) :
    Function.Surjective (GradedModule.secPiFwd D I)
def

secPiEquiv

L222 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_pi.ProjSpaceCech.GradedModule.secPiEquiv
Documentation

The equivalence between product module fraction sections and the finite product of component sections.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_pi
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section PiEquiv
variable {R : Type u} [CommRing R] {n : ℕ}
variable {ι : Type} [Fintype ι] (D : ι → GradedModule R n)
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · statement
def GradedModule.secPiEquiv (I : Finset (Fin (n + 1))) :
    GradedModule.sec (GradedModule.pi D) I ≃ₗ[R] (∀ k, GradedModule.sec (D k) I)
def

cochainPiEquiv

L229 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_pi.ProjSpaceCech.GradedModule.cochainPiEquiv
Documentation

The equivalence taking product graded module cochains to component cochains.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_pi
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section PiEquiv
variable {R : Type u} [CommRing R] {n : ℕ}
variable {ι : Type} [Fintype ι] (D : ι → GradedModule R n)
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · statement
def GradedModule.cochainPiEquiv (i : ℕ) :
    GradedModule.cochain (GradedModule.pi D) i
      ≃ₗ[R] (∀ k, GradedModule.cochain (D k) i)
theorem

cochainPiEquiv_apply

L236 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_pi.ProjSpaceCech.GradedModule.cochainPiEquiv_apply
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_pi
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section PiEquiv
variable {R : Type u} [CommRing R] {n : ℕ}
variable {ι : Type} [Fintype ι] (D : ι → GradedModule R n)
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · statement
theorem GradedModule.cochainPiEquiv_apply (i : ℕ)
    (f : GradedModule.cochain (GradedModule.pi D) i)
    (k : ι) (s : Idx n i) :
    GradedModule.cochainPiEquiv D i f k s
      = GradedModule.secPiFwd D (Idx.img n s) (f s) k
def

piAltd

L245 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_pi.ProjSpaceCech.GradedModule.piAltd
Documentation

The componentwise differential on the product of graded module cochain spaces.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_pi
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section PiEquiv
variable {R : Type u} [CommRing R] {n : ℕ}
variable {ι : Type} [Fintype ι] (D : ι → GradedModule R n)
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · statement
def GradedModule.piAltd (i : ℕ) :
    (∀ k, GradedModule.cochain (D k) i) →ₗ[R] (∀ k, GradedModule.cochain (D k) (i + 1))
theorem

cochainPiEquiv_comm

L250 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_pi.ProjSpaceCech.GradedModule.cochainPiEquiv_comm
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_pi
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section PiEquiv
variable {R : Type u} [CommRing R] {n : ℕ}
variable {ι : Type} [Fintype ι] (D : ι → GradedModule R n)
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · statement
theorem GradedModule.cochainPiEquiv_comm (i : ℕ) :
    (GradedModule.piAltd D i).comp (GradedModule.cochainPiEquiv D i).toLinearMap
      = (GradedModule.cochainPiEquiv D (i + 1)).toLinearMap.comp
          (GradedModule.d (GradedModule.pi D) i)
theorem

cochainPiEquiv_ker

L266 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_pi.ProjSpaceCech.GradedModule.cochainPiEquiv_ker
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_pi
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section PiEquiv
variable {R : Type u} [CommRing R] {n : ℕ}
variable {ι : Type} [Fintype ι] (D : ι → GradedModule R n)
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · statement
theorem GradedModule.cochainPiEquiv_ker (i : ℕ) :
    (LinearMap.ker (GradedModule.d (GradedModule.pi D) i)).map
        (GradedModule.cochainPiEquiv D i).toLinearMap
      = LinearMap.ker (GradedModule.piAltd D i)
theorem

cochainPiEquiv_range

L279 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_pi.ProjSpaceCech.GradedModule.cochainPiEquiv_range
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_pi
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section PiEquiv
variable {R : Type u} [CommRing R] {n : ℕ}
variable {ι : Type} [Fintype ι] (D : ι → GradedModule R n)
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · statement
theorem GradedModule.cochainPiEquiv_range (i : ℕ) :
    (LinearMap.range (GradedModule.d (GradedModule.pi D) i)).map
        (GradedModule.cochainPiEquiv D (i + 1)).toLinearMap
      = LinearMap.range (GradedModule.piAltd D i)
theorem

ker_piAltd

L289 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_pi.ProjSpaceCech.GradedModule.ker_piAltd
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_pi
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section PiEquiv
variable {R : Type u} [CommRing R] {n : ℕ}
variable {ι : Type} [Fintype ι] (D : ι → GradedModule R n)
open scoped _root_.ProjSpaceCech.GradedModule in
omit [Fintype ι] in
Lean source · full declaration
theorem GradedModule.ker_piAltd (i : ℕ) :
    LinearMap.ker (GradedModule.piAltd D i)
      = Submodule.pi Set.univ (fun k => LinearMap.ker (GradedModule.d (D k) i)) := by
  ext f
  simp only [LinearMap.mem_ker, GradedModule.piAltd, LinearMap.pi_apply, LinearMap.comp_apply,
    LinearMap.proj_apply, Submodule.mem_pi, Set.mem_univ, forall_true_left, funext_iff,
    Pi.zero_apply]
theorem

range_piAltd

L299 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_pi.ProjSpaceCech.GradedModule.range_piAltd
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_pi
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section PiEquiv
variable {R : Type u} [CommRing R] {n : ℕ}
variable {ι : Type} [Fintype ι] (D : ι → GradedModule R n)
open scoped _root_.ProjSpaceCech.GradedModule in
omit [Fintype ι] in
Lean source · full declaration
theorem GradedModule.range_piAltd (i : ℕ) :
    LinearMap.range (GradedModule.piAltd D i)
      = Submodule.pi Set.univ (fun k => LinearMap.range (GradedModule.d (D k) i)) := by
  refine le_antisymm ?_ ?_
  · rintro g ⟨f, rfl⟩ k _; exact ⟨f k, rfl⟩
  · intro g hg
    classical
    have hk : ∀ k, ∃ f, GradedModule.d (D k) i f = g k :=
      fun k => hg k (Set.mem_univ k)
    choose f hf using hk
    exact ⟨f, funext hf⟩
def

kerPiEquiv

L316 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_pi.ProjSpaceCech.GradedModule.kerPiEquiv
Documentation

The equivalence between the kernel of the product differential and the product of component kernels.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_pi
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section PiEquiv
variable {R : Type u} [CommRing R] {n : ℕ}
variable {ι : Type} [Fintype ι] (D : ι → GradedModule R n)
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · statement
def GradedModule.kerPiEquiv (i : ℕ) :
    ↥(LinearMap.ker (GradedModule.d (GradedModule.pi D) i))
      ≃ₗ[R] (∀ k, ↥(LinearMap.ker (GradedModule.d (D k) i)))
theorem

kerPiEquiv_apply_coe

L325 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_pi.ProjSpaceCech.GradedModule.kerPiEquiv_apply_coe
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_pi
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section PiEquiv
variable {R : Type u} [CommRing R] {n : ℕ}
variable {ι : Type} [Fintype ι] (D : ι → GradedModule R n)
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · statement
theorem GradedModule.kerPiEquiv_apply_coe (i : ℕ)
    (x : ↥(LinearMap.ker (GradedModule.d (GradedModule.pi D) i))) (k : ι) :
    (GradedModule.kerPiEquiv D i x k).1
      = GradedModule.cochainPiEquiv D i x.1 k
theorem

kerPiEquiv_comap_range

L345 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_pi.ProjSpaceCech.GradedModule.kerPiEquiv_comap_range
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_pi
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section PiEquiv
variable {R : Type u} [CommRing R] {n : ℕ}
variable {ι : Type} [Fintype ι] (D : ι → GradedModule R n)
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · full declaration
theorem GradedModule.kerPiEquiv_comap_range (j : ℕ) :
    Submodule.map (GradedModule.kerPiEquiv D (j + 1)).toLinearMap
        ((LinearMap.range (GradedModule.d (GradedModule.pi D) j)).comap
          (LinearMap.ker (GradedModule.d (GradedModule.pi D) (j + 1))).subtype)
      = Submodule.pi Set.univ (fun k =>
          (LinearMap.range (GradedModule.d (D k) j)).comap
            (LinearMap.ker (GradedModule.d (D k) (j + 1))).subtype) := by
  have hmain : ∀ (y : GradedModule.cochain (GradedModule.pi D) (j + 1)),
      y ∈ LinearMap.range (GradedModule.d (GradedModule.pi D) j)
        ↔ ∀ k, GradedModule.cochainPiEquiv D (j + 1) y k
            ∈ LinearMap.range (GradedModule.d (D k) j) := by
    intro y
    have hstep : (∀ k, GradedModule.cochainPiEquiv D (j + 1) y k
        ∈ LinearMap.range (GradedModule.d (D k) j))
          ↔ GradedModule.cochainPiEquiv D (j + 1) y
              ∈ LinearMap.range (GradedModule.piAltd D j) := by
      rw [GradedModule.range_piAltd]
      exact ⟨fun h k _ => h k, fun h k => h k (Set.mem_univ k)⟩
    rw [hstep, ← GradedModule.cochainPiEquiv_range D j, Submodule.mem_map_equiv,
      LinearEquiv.symm_apply_apply]
  refine le_antisymm ?_ ?_
  · rw [Submodule.map_le_iff_le_comap]
    rintro ⟨y, hy⟩ hyr
    simp only [Submodule.mem_comap, Submodule.coe_subtype] at hyr
    simp only [Submodule.mem_comap, LinearEquiv.coe_coe, Submodule.mem_pi, Set.mem_univ,
      forall_true_left]
    intro k
    change (GradedModule.kerPiEquiv D (j + 1) ⟨y, hy⟩ k).1
      ∈ LinearMap.range (GradedModule.d (D k) j)
    rw [GradedModule.kerPiEquiv_apply_coe]
    exact (hmain y).mp hyr k
  · intro z hz
    obtain ⟨⟨y, hy⟩, hyz⟩ := (GradedModule.kerPiEquiv D (j + 1)).surjective z
    refine ⟨⟨y, hy⟩, ?_, hyz⟩
    change y ∈ LinearMap.range (GradedModule.d (GradedModule.pi D) j)
    refine (hmain y).mpr fun k => ?_
    rw [← GradedModule.kerPiEquiv_apply_coe D (j + 1) ⟨y, hy⟩ k]
    have hzk := hz k (Set.mem_univ k)
    rw [← hyz] at hzk
    simp only at hzk
    exact hzk
def

HPiEquiv

L392 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_pi.ProjSpaceCech.GradedModule.HPiEquiv
Documentation

The equivalence between the Cech cohomology of a finite product and the product of component cohomologies.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_pi
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section PiEquiv
variable {R : Type u} [CommRing R] {n : ℕ}
variable {ι : Type} [Fintype ι] (D : ι → GradedModule R n)
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · statement
def GradedModule.HPiEquiv (i : ℕ) :
    GradedModule.H (GradedModule.pi D) i ≃ₗ[R] (∀ k, GradedModule.H (D k) i)
theorem

nonempty_HEquiv_pi

L407 ↗
ProjSpaceCech.GradedModule.nonempty_HEquiv_pi
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_pi
universe u
noncomputable section
open Finset Function MvPolynomial
Lean source · statement
theorem _root_.ProjSpaceCech.GradedModule.nonempty_HEquiv_pi {R : Type u} [CommRing R] {n : ℕ} {ι
    : Type} [Fintype ι] (D : ι → ProjSpaceCech.GradedModule R n) (i : ℕ) :
    Nonempty (ProjSpaceCech.GradedModule.H (ProjSpaceCech.GradedModule.pi D) i ≃ₗ[R] (∀ k,
      ProjSpaceCech.GradedModule.H (D k) i))

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