Module

OModulePresheaf_nonempty_cech_baseChange_equiv_of_locallyTrivial.lean

Nyll.AlgebraicCurves.Cohomology.Cech.OModulePresheaf_nonempty_cech_baseChange_equiv_of_locallyTrivial

16 declarations indexed from sourceView source ↗

Module documentation

Čech cohomology base-change equivalences for locally trivial module presheaves.

Imports4

Imported by7

theorem

apply_f

L49 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cech_baseChange_equiv_of_locallyTrivial.LinearMap.HomologyTransport.apply_f

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_nonempty_cech_baseChange_equiv_of_locallyTrivial
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
noncomputable section
namespace LinearMap
open _root_.LinearMap
namespace HomologyTransport
open _root_.LinearMap
variable {S : Type u} [CommRing S]
variable {P₀ P₁ P₂ Q₀ Q₁ Q₂ : Type u}
  [AddCommGroup P₀] [Module S P₀] [AddCommGroup P₁] [Module S P₁] [AddCommGroup P₂] [Module S P₂]
  [AddCommGroup Q₀] [Module S Q₀] [AddCommGroup Q₁] [Module S Q₁] [AddCommGroup Q₂] [Module S Q₂]
variable (e₀ : P₀ ≃ₗ[S] Q₀) (e₁ : P₁ ≃ₗ[S] Q₁) (e₂ : P₂ ≃ₗ[S] Q₂)
variable (f : P₀ →ₗ[S] P₁) (g : P₁ →ₗ[S] P₂) (f' : Q₀ →ₗ[S] Q₁) (g' : Q₁ →ₗ[S] Q₂)
variable (hf : e₁.toLinearMap ∘ₗ f = f' ∘ₗ e₀.toLinearMap) (hg : e₂.toLinearMap ∘ₗ g = g' ∘ₗ
  e₁.toLinearMap)
include hf in

Lean source · statement

theorem apply_f (x : P₀) : e₁ (f x) = f' (e₀ x)

theorem

comap_ker

L53 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cech_baseChange_equiv_of_locallyTrivial.LinearMap.HomologyTransport.comap_ker

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_nonempty_cech_baseChange_equiv_of_locallyTrivial
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
noncomputable section
namespace LinearMap
open _root_.LinearMap
namespace HomologyTransport
open _root_.LinearMap
variable {S : Type u} [CommRing S]
variable {P₀ P₁ P₂ Q₀ Q₁ Q₂ : Type u}
  [AddCommGroup P₀] [Module S P₀] [AddCommGroup P₁] [Module S P₁] [AddCommGroup P₂] [Module S P₂]
  [AddCommGroup Q₀] [Module S Q₀] [AddCommGroup Q₁] [Module S Q₁] [AddCommGroup Q₂] [Module S Q₂]
variable (e₀ : P₀ ≃ₗ[S] Q₀) (e₁ : P₁ ≃ₗ[S] Q₁) (e₂ : P₂ ≃ₗ[S] Q₂)
variable (f : P₀ →ₗ[S] P₁) (g : P₁ →ₗ[S] P₂) (f' : Q₀ →ₗ[S] Q₁) (g' : Q₁ →ₗ[S] Q₂)
variable (hf : e₁.toLinearMap ∘ₗ f = f' ∘ₗ e₀.toLinearMap) (hg : e₂.toLinearMap ∘ₗ g = g' ∘ₗ
  e₁.toLinearMap)
include hf in

Lean source · statement

theorem comap_ker : (LinearMap.ker f').comap e₀.toLinearMap = LinearMap.ker f

def

kerEquiv

L59 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cech_baseChange_equiv_of_locallyTrivial.LinearMap.HomologyTransport.kerEquiv

Documentation

The equivalence of kernels induced by a commutative square of linear equivalences.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_nonempty_cech_baseChange_equiv_of_locallyTrivial
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
noncomputable section
namespace LinearMap
open _root_.LinearMap
namespace HomologyTransport
open _root_.LinearMap
variable {S : Type u} [CommRing S]
variable {P₀ P₁ P₂ Q₀ Q₁ Q₂ : Type u}
  [AddCommGroup P₀] [Module S P₀] [AddCommGroup P₁] [Module S P₁] [AddCommGroup P₂] [Module S P₂]
  [AddCommGroup Q₀] [Module S Q₀] [AddCommGroup Q₁] [Module S Q₁] [AddCommGroup Q₂] [Module S Q₂]
variable (e₀ : P₀ ≃ₗ[S] Q₀) (e₁ : P₁ ≃ₗ[S] Q₁) (e₂ : P₂ ≃ₗ[S] Q₂)
variable (f : P₀ →ₗ[S] P₁) (g : P₁ →ₗ[S] P₂) (f' : Q₀ →ₗ[S] Q₁) (g' : Q₁ →ₗ[S] Q₂)
variable (hf : e₁.toLinearMap ∘ₗ f = f' ∘ₗ e₀.toLinearMap) (hg : e₂.toLinearMap ∘ₗ g = g' ∘ₗ
  e₁.toLinearMap)

Lean source · statement

def kerEquiv : LinearMap.ker f ≃ₗ[S] LinearMap.ker f'

theorem

kerEquiv_apply_coe

L62 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cech_baseChange_equiv_of_locallyTrivial.LinearMap.HomologyTransport.kerEquiv_apply_coe

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_nonempty_cech_baseChange_equiv_of_locallyTrivial
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
noncomputable section
namespace LinearMap
open _root_.LinearMap
namespace HomologyTransport
open _root_.LinearMap
variable {S : Type u} [CommRing S]
variable {P₀ P₁ P₂ Q₀ Q₁ Q₂ : Type u}
  [AddCommGroup P₀] [Module S P₀] [AddCommGroup P₁] [Module S P₁] [AddCommGroup P₂] [Module S P₂]
  [AddCommGroup Q₀] [Module S Q₀] [AddCommGroup Q₁] [Module S Q₁] [AddCommGroup Q₂] [Module S Q₂]
variable (e₀ : P₀ ≃ₗ[S] Q₀) (e₁ : P₁ ≃ₗ[S] Q₁) (e₂ : P₂ ≃ₗ[S] Q₂)
variable (f : P₀ →ₗ[S] P₁) (g : P₁ →ₗ[S] P₂) (f' : Q₀ →ₗ[S] Q₁) (g' : Q₁ →ₗ[S] Q₂)
variable (hf : e₁.toLinearMap ∘ₗ f = f' ∘ₗ e₀.toLinearMap) (hg : e₂.toLinearMap ∘ₗ g = g' ∘ₗ
  e₁.toLinearMap)

Lean source · statement

theorem kerEquiv_apply_coe (x : LinearMap.ker f) : (kerEquiv e₀ e₁ f f' hf x : Q₀) = e₀ x

theorem

comap_kerEquiv_comap_range

L65 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cech_baseChange_equiv_of_locallyTrivial.LinearMap.HomologyTransport.comap_kerEquiv_comap_range

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_nonempty_cech_baseChange_equiv_of_locallyTrivial
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
noncomputable section
namespace LinearMap
open _root_.LinearMap
namespace HomologyTransport
open _root_.LinearMap
variable {S : Type u} [CommRing S]
variable {P₀ P₁ P₂ Q₀ Q₁ Q₂ : Type u}
  [AddCommGroup P₀] [Module S P₀] [AddCommGroup P₁] [Module S P₁] [AddCommGroup P₂] [Module S P₂]
  [AddCommGroup Q₀] [Module S Q₀] [AddCommGroup Q₁] [Module S Q₁] [AddCommGroup Q₂] [Module S Q₂]
variable (e₀ : P₀ ≃ₗ[S] Q₀) (e₁ : P₁ ≃ₗ[S] Q₁) (e₂ : P₂ ≃ₗ[S] Q₂)
variable (f : P₀ →ₗ[S] P₁) (g : P₁ →ₗ[S] P₂) (f' : Q₀ →ₗ[S] Q₁) (g' : Q₁ →ₗ[S] Q₂)
variable (hf : e₁.toLinearMap ∘ₗ f = f' ∘ₗ e₀.toLinearMap) (hg : e₂.toLinearMap ∘ₗ g = g' ∘ₗ
  e₁.toLinearMap)
include hf hg in

Lean source · statement

theorem comap_kerEquiv_comap_range :
    ((LinearMap.range f').comap (LinearMap.ker g').subtype).comap (kerEquiv e₁ e₂ g g'
      hg).toLinearMap
      = (LinearMap.range f).comap (LinearMap.ker g).subtype

theorem

map_kerEquiv_comap_range

L80 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cech_baseChange_equiv_of_locallyTrivial.LinearMap.HomologyTransport.map_kerEquiv_comap_range

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_nonempty_cech_baseChange_equiv_of_locallyTrivial
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
noncomputable section
namespace LinearMap
open _root_.LinearMap
namespace HomologyTransport
open _root_.LinearMap
variable {S : Type u} [CommRing S]
variable {P₀ P₁ P₂ Q₀ Q₁ Q₂ : Type u}
  [AddCommGroup P₀] [Module S P₀] [AddCommGroup P₁] [Module S P₁] [AddCommGroup P₂] [Module S P₂]
  [AddCommGroup Q₀] [Module S Q₀] [AddCommGroup Q₁] [Module S Q₁] [AddCommGroup Q₂] [Module S Q₂]
variable (e₀ : P₀ ≃ₗ[S] Q₀) (e₁ : P₁ ≃ₗ[S] Q₁) (e₂ : P₂ ≃ₗ[S] Q₂)
variable (f : P₀ →ₗ[S] P₁) (g : P₁ →ₗ[S] P₂) (f' : Q₀ →ₗ[S] Q₁) (g' : Q₁ →ₗ[S] Q₂)
variable (hf : e₁.toLinearMap ∘ₗ f = f' ∘ₗ e₀.toLinearMap) (hg : e₂.toLinearMap ∘ₗ g = g' ∘ₗ
  e₁.toLinearMap)
include hf hg in

Lean source · statement

theorem map_kerEquiv_comap_range :
    ((LinearMap.range f).comap (LinearMap.ker g).subtype).map (kerEquiv e₁ e₂ g g' hg).toLinearMap
      = (LinearMap.range f').comap (LinearMap.ker g').subtype

theorem

subtype_baseChange_injective

L98 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cech_baseChange_equiv_of_locallyTrivial.LinearMap.FlatKerBC.subtype_baseChange_injective

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_nonempty_cech_baseChange_equiv_of_locallyTrivial
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
noncomputable section
namespace LinearMap
open _root_.LinearMap
namespace FlatKerBC
open _root_.LinearMap
variable {R : Type u} [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
variable {M₀ M₁ M₂ : Type u} [AddCommGroup M₀] [Module R M₀] [AddCommGroup M₁] [Module R M₁]
  [AddCommGroup M₂] [Module R M₂]
variable (f : M₀ →ₗ[R] M₁) (g : M₁ →ₗ[R] M₂)

Lean source · statement

theorem subtype_baseChange_injective [Module.Flat R A] :
    Function.Injective ((LinearMap.ker g).subtype.baseChange A)

theorem

range_subtype_baseChange

L103 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cech_baseChange_equiv_of_locallyTrivial.LinearMap.FlatKerBC.range_subtype_baseChange

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_nonempty_cech_baseChange_equiv_of_locallyTrivial
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
noncomputable section
namespace LinearMap
open _root_.LinearMap
namespace FlatKerBC
open _root_.LinearMap
variable {R : Type u} [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
variable {M₀ M₁ M₂ : Type u} [AddCommGroup M₀] [Module R M₀] [AddCommGroup M₁] [Module R M₁]
  [AddCommGroup M₂] [Module R M₂]
variable (f : M₀ →ₗ[R] M₁) (g : M₁ →ₗ[R] M₂)

Lean source · statement

theorem range_subtype_baseChange [Module.Flat R A] :
    LinearMap.range ((LinearMap.ker g).subtype.baseChange A) = LinearMap.ker (g.baseChange A)

def

theta

L112 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cech_baseChange_equiv_of_locallyTrivial.LinearMap.FlatKerBC.theta

Documentation

The canonical equivalence between the base change of a kernel and the base-changed kernel.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_nonempty_cech_baseChange_equiv_of_locallyTrivial
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
noncomputable section
namespace LinearMap
open _root_.LinearMap
namespace FlatKerBC
open _root_.LinearMap
variable {R : Type u} [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
variable {M₀ M₁ M₂ : Type u} [AddCommGroup M₀] [Module R M₀] [AddCommGroup M₁] [Module R M₁]
  [AddCommGroup M₂] [Module R M₂]
variable (f : M₀ →ₗ[R] M₁) (g : M₁ →ₗ[R] M₂)

Lean source · statement

def theta [Module.Flat R A] : A ⊗[R] LinearMap.ker g ≃ₗ[A] LinearMap.ker (g.baseChange A)

theorem

theta_apply_coe

L116 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cech_baseChange_equiv_of_locallyTrivial.LinearMap.FlatKerBC.theta_apply_coe

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_nonempty_cech_baseChange_equiv_of_locallyTrivial
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
noncomputable section
namespace LinearMap
open _root_.LinearMap
namespace FlatKerBC
open _root_.LinearMap
variable {R : Type u} [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
variable {M₀ M₁ M₂ : Type u} [AddCommGroup M₀] [Module R M₀] [AddCommGroup M₁] [Module R M₁]
  [AddCommGroup M₂] [Module R M₂]
variable (f : M₀ →ₗ[R] M₁) (g : M₁ →ₗ[R] M₂)

Lean source · statement

theorem theta_apply_coe [Module.Flat R A] (z : A ⊗[R] LinearMap.ker g) :
    (theta A g z : A ⊗[R] M₁) = ((LinearMap.ker g).subtype.baseChange A) z

def

toKer

L122 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cech_baseChange_equiv_of_locallyTrivial.LinearMap.FlatKerBC.toKer

Documentation

The first differential with codomain restricted to the kernel of the next differential.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_nonempty_cech_baseChange_equiv_of_locallyTrivial
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
noncomputable section
namespace LinearMap
open _root_.LinearMap
namespace FlatKerBC
open _root_.LinearMap
variable {R : Type u} [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
variable {M₀ M₁ M₂ : Type u} [AddCommGroup M₀] [Module R M₀] [AddCommGroup M₁] [Module R M₁]
  [AddCommGroup M₂] [Module R M₂]
variable (f : M₀ →ₗ[R] M₁) (g : M₁ →ₗ[R] M₂)
variable (hgf : g ∘ₗ f = 0)

Lean source · statement

def toKer : M₀ →ₗ[R] LinearMap.ker g

theorem

subtype_comp_toKer

L126 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cech_baseChange_equiv_of_locallyTrivial.LinearMap.FlatKerBC.subtype_comp_toKer

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_nonempty_cech_baseChange_equiv_of_locallyTrivial
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
noncomputable section
namespace LinearMap
open _root_.LinearMap
namespace FlatKerBC
open _root_.LinearMap
variable {R : Type u} [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
variable {M₀ M₁ M₂ : Type u} [AddCommGroup M₀] [Module R M₀] [AddCommGroup M₁] [Module R M₁]
  [AddCommGroup M₂] [Module R M₂]
variable (f : M₀ →ₗ[R] M₁) (g : M₁ →ₗ[R] M₂)
variable (hgf : g ∘ₗ f = 0)

Lean source · statement

theorem subtype_comp_toKer : (LinearMap.ker g).subtype ∘ₗ toKer f g hgf = f

theorem

range_toKer

L128 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cech_baseChange_equiv_of_locallyTrivial.LinearMap.FlatKerBC.range_toKer

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_nonempty_cech_baseChange_equiv_of_locallyTrivial
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
noncomputable section
namespace LinearMap
open _root_.LinearMap
namespace FlatKerBC
open _root_.LinearMap
variable {R : Type u} [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
variable {M₀ M₁ M₂ : Type u} [AddCommGroup M₀] [Module R M₀] [AddCommGroup M₁] [Module R M₁]
  [AddCommGroup M₂] [Module R M₂]
variable (f : M₀ →ₗ[R] M₁) (g : M₁ →ₗ[R] M₂)
variable (hgf : g ∘ₗ f = 0)

Lean source · statement

theorem range_toKer : LinearMap.range (toKer f g hgf) = (LinearMap.range f).comap (LinearMap.ker
  g).subtype

theorem

comap_theta

L137 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cech_baseChange_equiv_of_locallyTrivial.LinearMap.FlatKerBC.comap_theta

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_nonempty_cech_baseChange_equiv_of_locallyTrivial
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
noncomputable section
namespace LinearMap
open _root_.LinearMap
namespace FlatKerBC
open _root_.LinearMap
variable {R : Type u} [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
variable {M₀ M₁ M₂ : Type u} [AddCommGroup M₀] [Module R M₀] [AddCommGroup M₁] [Module R M₁]
  [AddCommGroup M₂] [Module R M₂]
variable (f : M₀ →ₗ[R] M₁) (g : M₁ →ₗ[R] M₂)
variable (hgf : g ∘ₗ f = 0)
include hgf in

Lean source · statement

theorem comap_theta [Module.Flat R A] :
    ((LinearMap.range (f.baseChange A)).comap (LinearMap.ker (g.baseChange A)).subtype).comap
        (theta A g).toLinearMap
      = LinearMap.range ((toKer f g hgf).baseChange A)

theorem

nonempty_quotEquiv

L155 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cech_baseChange_equiv_of_locallyTrivial.LinearMap.FlatKerBC.nonempty_quotEquiv

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_nonempty_cech_baseChange_equiv_of_locallyTrivial
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
noncomputable section
namespace LinearMap
open _root_.LinearMap
namespace FlatKerBC
open _root_.LinearMap
variable {R : Type u} [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
variable {M₀ M₁ M₂ : Type u} [AddCommGroup M₀] [Module R M₀] [AddCommGroup M₁] [Module R M₁]
  [AddCommGroup M₂] [Module R M₂]
variable (f : M₀ →ₗ[R] M₁) (g : M₁ →ₗ[R] M₂)
variable (hgf : g ∘ₗ f = 0)
include hgf in

Lean source · statement

theorem nonempty_quotEquiv :
    Nonempty (((A ⊗[R] LinearMap.ker g) ⧸ LinearMap.range ((toKer f g hgf).baseChange A))
      ≃ₗ[A] A ⊗[R] (LinearMap.ker g ⧸ (LinearMap.range f).comap (LinearMap.ker g).subtype))

theorem

nonempty_cech_baseChange_equiv_of_locallyTrivial

L180 ↗

AlgebraicGeometry.OModulePresheaf.nonempty_cech_baseChange_equiv_of_locallyTrivial

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_nonempty_cech_baseChange_equiv_of_locallyTrivial
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
open LinearMap.HomologyTransport LinearMap.FlatKerBC in

Lean source · statement

theorem _root_.AlgebraicGeometry.OModulePresheaf.nonempty_cech_baseChange_equiv_of_locallyTrivial
    {R : Type u} [CommRing R] {X : Scheme.{u}} (π : X ⟶ Spec (.of R)) [IsSeparated π]
    (𝒰 : X.OrderedAffineCover) (M : X.Modules)
    (htriv : ∀ x : X, ∃ (V : X.Opens), x ∈ V ∧
      Nonempty ((Scheme.Modules.pullback V.ι).obj M ≅ SheafOfModules.unit V.toScheme.ringCatSheaf))
    (A : Type u) [CommRing A] [Algebra R A] :
    (Nonempty ((OModulePresheaf.ofModules (Limits.pullback.snd π
      (Scheme.TwoAffineOpenCover.specMap R A))
          ((Scheme.Modules.pullback
            (Limits.pullback.fst π (Scheme.TwoAffineOpenCover.specMap R A))).obj M)).H0
              (𝒰.baseChange π A)
        ≃ₗ[A] LinearMap.ker (((OModulePresheaf.ofModules π M).d 𝒰 0).baseChange A)) ∧
      ∀ i : ℕ, ∃ φ : LinearMap.ker (((OModulePresheaf.ofModules π M).d 𝒰 (i + 1)).baseChange A)
        →ₗ[A]
          (OModulePresheaf.ofModules (Limits.pullback.snd π (Scheme.TwoAffineOpenCover.specMap R A))
          ((Scheme.Modules.pullback
            (Limits.pullback.fst π (Scheme.TwoAffineOpenCover.specMap R A))).obj M)).HSucc
              (𝒰.baseChange π A) i,
        Function.Surjective φ ∧
          LinearMap.ker φ = (LinearMap.range (((OModulePresheaf.ofModules π M).d 𝒰 i).baseChange
            A)).comap
            (LinearMap.ker (((OModulePresheaf.ofModules π M).d 𝒰 (i + 1)).baseChange A)).subtype) ∧
    (Module.Flat R A →
      Nonempty ((OModulePresheaf.ofModules (Limits.pullback.snd π
        (Scheme.TwoAffineOpenCover.specMap R A))
          ((Scheme.Modules.pullback
            (Limits.pullback.fst π (Scheme.TwoAffineOpenCover.specMap R A))).obj M)).H0
              (𝒰.baseChange π A)
          ≃ₗ[A] A ⊗[R] (OModulePresheaf.ofModules π M).H0 𝒰) ∧
      ∀ i : ℕ, Nonempty ((OModulePresheaf.ofModules (Limits.pullback.snd π
        (Scheme.TwoAffineOpenCover.specMap R A))
          ((Scheme.Modules.pullback
            (Limits.pullback.fst π (Scheme.TwoAffineOpenCover.specMap R A))).obj M)).HSucc
              (𝒰.baseChange π A) i
          ≃ₗ[A] A ⊗[R] (OModulePresheaf.ofModules π M).HSucc 𝒰 i))

Module documentation

Declarations