NYLL
Module

CoherentBaseChange_TwoTermComplex_one_tmul_ne_zero_of_forall_nonempty_H0_linearEquiv.lean

Nyll.AlgebraicCurves.Cohomology.Cech.CoherentBaseChange_TwoTermComplex_one_tmul_ne_zero_of_forall_nonempty_H0_linearEquiv
13 declarations indexed from sourceView source ↗

Module documentation

Coherent Base Change Two Term Complex one tmul ne zero of forall nonempty H0 linear Equiv

Imports4
Imported by2

Declarations

theorem

baseChange_rTensor

L41 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermOneTensorNonzero.P2mTwoTermH0Unimodular.baseChange_rTensor
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermOneTensorNonzero
universe u
open TensorProduct
noncomputable section
namespace P2mTwoTermH0Unimodular
variable {R : Type u} [CommRing R]
section Naturality
variable {A B : Type u} [CommRing A] [Algebra R A] [CommRing B] [Algebra R B]
  {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
Lean source · statement
theorem baseChange_rTensor (d : C0 →ₗ[R] C1) (φ : A →ₗ[R] B) (x : A ⊗[R] C0) :
    (d.baseChange B) (φ.rTensor C0 x) = φ.rTensor C1 (d.baseChange A x)
theorem

lid_baseChange_apply

L47 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermOneTensorNonzero.P2mTwoTermH0Unimodular.lid_baseChange_apply
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermOneTensorNonzero
universe u
open TensorProduct
noncomputable section
namespace P2mTwoTermH0Unimodular
variable {R : Type u} [CommRing R]
section Naturality
variable {A B : Type u} [CommRing A] [Algebra R A] [CommRing B] [Algebra R B]
  {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
Lean source · statement
theorem lid_baseChange_apply (d : C0 →ₗ[R] C1) (x : R ⊗[R] C0) :
    TensorProduct.lid R C1 (d.baseChange R x) = d (TensorProduct.lid R C0 x)
def

opModule

L61 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermOneTensorNonzero.P2mTwoTermH0Unimodular.opModule
Documentation

The opposite-ring action induced by commutativity of the base ring.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermOneTensorNonzero
universe u
open TensorProduct
noncomputable section
namespace P2mTwoTermH0Unimodular
variable {R : Type u} [CommRing R]
section SqZero
variable (R) (M : Type u) [AddCommGroup M] [Module R M]
Lean source · statement
def opModule : Module Rᵐᵒᵖ M
theorem

op_smul_eq

L65 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermOneTensorNonzero.P2mTwoTermH0Unimodular.op_smul_eq
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermOneTensorNonzero
universe u
open TensorProduct
noncomputable section
namespace P2mTwoTermH0Unimodular
variable {R : Type u} [CommRing R]
section SqZero
variable (R) (M : Type u) [AddCommGroup M] [Module R M]
attribute [local instance] opModule
Lean source · statement
theorem op_smul_eq (r : R) (m : M) : (MulOpposite.op r) • m = r • m
instance

isCentralScalar

L67 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermOneTensorNonzero.P2mTwoTermH0Unimodular.isCentralScalar
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermOneTensorNonzero
universe u
open TensorProduct
noncomputable section
namespace P2mTwoTermH0Unimodular
variable {R : Type u} [CommRing R]
section SqZero
variable (R) (M : Type u) [AddCommGroup M] [Module R M]
attribute [local instance] opModule
Lean source · statement
instance isCentralScalar : IsCentralScalar R M
instance

isScalarTower_op

L69 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermOneTensorNonzero.P2mTwoTermH0Unimodular.isScalarTower_op
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermOneTensorNonzero
universe u
open TensorProduct
noncomputable section
namespace P2mTwoTermH0Unimodular
variable {R : Type u} [CommRing R]
section SqZero
variable (R) (M : Type u) [AddCommGroup M] [Module R M]
attribute [local instance] opModule
Lean source · statement
instance isScalarTower_op : IsScalarTower R Rᵐᵒᵖ M
instance

smulCommClass_op

L74 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermOneTensorNonzero.P2mTwoTermH0Unimodular.smulCommClass_op
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermOneTensorNonzero
universe u
open TensorProduct
noncomputable section
namespace P2mTwoTermH0Unimodular
variable {R : Type u} [CommRing R]
section SqZero
variable (R) (M : Type u) [AddCommGroup M] [Module R M]
attribute [local instance] opModule
Lean source · statement
instance smulCommClass_op : SMulCommClass R Rᵐᵒᵖ M
theorem

inr_mul_eq

L82 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermOneTensorNonzero.P2mTwoTermH0Unimodular.inr_mul_eq
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermOneTensorNonzero
universe u
open TensorProduct
noncomputable section
namespace P2mTwoTermH0Unimodular
variable {R : Type u} [CommRing R]
section SqZero
variable (R) (M : Type u) [AddCommGroup M] [Module R M]
attribute [local instance] opModule
Lean source · statement
theorem inr_mul_eq (m : M) (x : TrivSqZeroExt R M) :
    (TrivSqZeroExt.inr m : TrivSqZeroExt R M) * x = TrivSqZeroExt.inr (x.fst • m)
theorem

inr_smul_eq

L99 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermOneTensorNonzero.P2mTwoTermH0Unimodular.inr_smul_eq
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermOneTensorNonzero
universe u
open TensorProduct
noncomputable section
namespace P2mTwoTermH0Unimodular
variable {R : Type u} [CommRing R]
section Main
variable (G : CoherentBaseChange.TwoTermComplex.{u, u} R)
variable (M : Type u) [AddCommGroup M] [Module R M]
attribute [local instance] opModule
Lean source · statement
theorem inr_smul_eq (m : M) (k : TrivSqZeroExt R M ⊗[R] G.C0) :
    (TrivSqZeroExt.inr m : TrivSqZeroExt R M) • k =
      (TrivSqZeroExt.inr m : TrivSqZeroExt R M) ⊗ₜ[R]
        TensorProduct.lid R G.C0 ((TrivSqZeroExt.fstHom R R M).toLinearMap.rTensor G.C0 k)
theorem

inr_tmul_eq_zero

L110 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermOneTensorNonzero.P2mTwoTermH0Unimodular.inr_tmul_eq_zero
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermOneTensorNonzero
universe u
open TensorProduct
noncomputable section
namespace P2mTwoTermH0Unimodular
variable {R : Type u} [CommRing R]
section Main
variable (G : CoherentBaseChange.TwoTermComplex.{u, u} R)
variable (M : Type u) [AddCommGroup M] [Module R M]
attribute [local instance] opModule
Lean source · statement
theorem inr_tmul_eq_zero (g₀ : G.C0) (h : ∀ m : M, (m ⊗ₜ[R] g₀ : M ⊗[R] G.C0) = 0) (m : M) (r : R) :
    ((TrivSqZeroExt.inr m : TrivSqZeroExt R M) ⊗ₜ[R] (r • g₀) : TrivSqZeroExt R M ⊗[R] G.C0) = 0
theorem

subsingleton_of_forall_tmul_eq_zero

L120 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermOneTensorNonzero.P2mTwoTermH0Unimodular.subsingleton_of_forall_tmul_eq_zero
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermOneTensorNonzero
universe u
open TensorProduct
noncomputable section
namespace P2mTwoTermH0Unimodular
variable {R : Type u} [CommRing R]
section Main
variable (G : CoherentBaseChange.TwoTermComplex.{u, u} R)
variable (M : Type u) [AddCommGroup M] [Module R M]
attribute [local instance] opModule
Lean source · statement
theorem subsingleton_of_forall_tmul_eq_zero (g₀ : G.C0)
    (hker : ∀ x : G.C0, G.d x = 0 → ∃ r : R, x = r • g₀)
    (ψ : G.H0 (TrivSqZeroExt R M) ≃ₗ[TrivSqZeroExt R M] TrivSqZeroExt R M)
    (h : ∀ m : M, (m ⊗ₜ[R] g₀ : M ⊗[R] G.C0) = 0) : Subsingleton M
theorem

main

L148 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermOneTensorNonzero.P2mTwoTermH0Unimodular.main
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermOneTensorNonzero
universe u
open TensorProduct
noncomputable section
namespace P2mTwoTermH0Unimodular
variable {R : Type u} [CommRing R]
section Main
variable (G : CoherentBaseChange.TwoTermComplex.{u, u} R)
variable (M : Type u) [AddCommGroup M] [Module R M]
attribute [local instance] opModule
Lean source · statement
theorem main (g₀ : G.C0)
    (hker : ∀ x : G.C0, G.d x = 0 → ∃ r : R, x = r • g₀)
    (hH0 : ∀ (C : Type u) [CommRing C] [Algebra R C], Nonempty (G.H0 C ≃ₗ[C] C))
    (C : Type u) [CommRing C] [Algebra R C] [Nontrivial C] :
    ((1 : C) ⊗ₜ[R] g₀ : C ⊗[R] G.C0) ≠ 0
theorem

one_tmul_ne_zero_of_forall_nonempty_H0_linearEquiv

L178 ↗
CoherentBaseChange.TwoTermComplex.one_tmul_ne_zero_of_forall_nonempty_H0_linearEquiv
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermOneTensorNonzero
universe u
open TensorProduct
attribute [local instance] P2mTwoTermH0Unimodular.isCentralScalar
attribute [local instance] P2mTwoTermH0Unimodular.isScalarTower_op
attribute [local instance] P2mTwoTermH0Unimodular.smulCommClass_op
Lean source · statement
theorem _root_.CoherentBaseChange.TwoTermComplex.one_tmul_ne_zero_of_forall_nonempty_H0_linearEquiv
    {R : Type u} [CommRing R] (G : CoherentBaseChange.TwoTermComplex.{u, u} R) (g₀ : G.C0)
    (hker : ∀ x : G.C0, G.d x = 0 → ∃ r : R, x = r • g₀)
    (hH0 : ∀ (C : Type u) [CommRing C] [Algebra R C], Nonempty (G.H0 C ≃ₗ[C] C))
    (C : Type u) [CommRing C] [Algebra R C] [Nontrivial C] :
    ((1 : C) ⊗ₜ[R] g₀ : C ⊗[R] G.C0) ≠ 0

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