Module

TwoChartCech_Cover_squareZeroUnit_cohomologous_iff_and_exists.lean

Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCech_Cover_squareZeroUnit_cohomologous_iff_and_exists

33 declarations indexed from sourceView source ↗

Module documentation

Two Chart Cech Cover square Zero Unit cohomologous iff and exists

Imports3

Nyll.SchemeTheory.Cohomology.Cech.TwoChartCech
Mathlib.Algebra.TrivSqZeroExt.Basic
Mathlib.LinearAlgebra.TensorProduct.Prod

Imported by2

def

red

L43 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit.P2mTJ2a.red

Documentation

Reduce the tensor product of a square-zero extension to its scalar component.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit
open scoped TensorProduct
open TrivSqZeroExt
universe u
namespace P2mTJ2a
noncomputable section
variable {K : Type u} [Field K]
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
section Decomp
variable (K V)
variable (B : Type u) [CommRing B] [Algebra K B]

Lean source · statement

def red : TrivSqZeroExt K V ⊗[K] B →ₐ[K] B

def

σ

L48 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit.P2mTJ2a.σ

Documentation

Project to the square-zero component and interchange the two tensor factors.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit
open scoped TensorProduct
open TrivSqZeroExt
universe u
namespace P2mTJ2a
noncomputable section
variable {K : Type u} [Field K]
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
section Decomp
variable (K V)
variable (B : Type u) [CommRing B] [Algebra K B]

Lean source · statement

def σ : TrivSqZeroExt K V ⊗[K] B →ₗ[K] B ⊗[K] V

def

incl

L53 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit.P2mTJ2a.incl

Documentation

Include the square-zero component after interchanging tensor factors.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit
open scoped TensorProduct
open TrivSqZeroExt
universe u
namespace P2mTJ2a
noncomputable section
variable {K : Type u} [Field K]
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
section Decomp
variable (K V)
variable (B : Type u) [CommRing B] [Algebra K B]

Lean source · statement

def incl : B ⊗[K] V →ₗ[K] TrivSqZeroExt K V ⊗[K] B

theorem

red_tmul

L59 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit.P2mTJ2a.red_tmul

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit
open scoped TensorProduct
open TrivSqZeroExt
universe u
namespace P2mTJ2a
noncomputable section
variable {K : Type u} [Field K]
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
section Decomp
variable (K V)
variable (B : Type u) [CommRing B] [Algebra K B]
variable {K V B}

Lean source · statement

theorem red_tmul (a : TrivSqZeroExt K V) (b : B) : red K V B (a ⊗ₜ b) = a.fst • b

theorem

σ_tmul

L64 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit.P2mTJ2a.σ_tmul

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit
open scoped TensorProduct
open TrivSqZeroExt
universe u
namespace P2mTJ2a
noncomputable section
variable {K : Type u} [Field K]
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
section Decomp
variable (K V)
variable (B : Type u) [CommRing B] [Algebra K B]
variable {K V B}
omit [Module Kᵐᵒᵖ V] [IsCentralScalar K V] in

Lean source · statement

theorem σ_tmul (a : TrivSqZeroExt K V) (b : B) : σ K V B (a ⊗ₜ b) = b ⊗ₜ a.snd

theorem

incl_tmul

L68 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit.P2mTJ2a.incl_tmul

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit
open scoped TensorProduct
open TrivSqZeroExt
universe u
namespace P2mTJ2a
noncomputable section
variable {K : Type u} [Field K]
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
section Decomp
variable (K V)
variable (B : Type u) [CommRing B] [Algebra K B]
variable {K V B}
omit [Module Kᵐᵒᵖ V] [IsCentralScalar K V] in

Lean source · statement

theorem incl_tmul (b : B) (v : V) : incl K V B (b ⊗ₜ v) = (TrivSqZeroExt.inr v)
  ⊗ₜ b

theorem

red_incl

L72 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit.P2mTJ2a.red_incl

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit
open scoped TensorProduct
open TrivSqZeroExt
universe u
namespace P2mTJ2a
noncomputable section
variable {K : Type u} [Field K]
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
section Decomp
variable (K V)
variable (B : Type u) [CommRing B] [Algebra K B]
variable {K V B}

Lean source · statement

theorem red_incl (w : B ⊗[K] V) : red K V B (incl K V B w) = 0

theorem

σ_incl

L78 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit.P2mTJ2a.σ_incl

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit
open scoped TensorProduct
open TrivSqZeroExt
universe u
namespace P2mTJ2a
noncomputable section
variable {K : Type u} [Field K]
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
section Decomp
variable (K V)
variable (B : Type u) [CommRing B] [Algebra K B]
variable {K V B}
omit [Module Kᵐᵒᵖ V] [IsCentralScalar K V] in

Lean source · statement

theorem σ_incl (w : B ⊗[K] V) : σ K V B (incl K V B w) = w

theorem

red_includeRight

L83 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit.P2mTJ2a.red_includeRight

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit
open scoped TensorProduct
open TrivSqZeroExt
universe u
namespace P2mTJ2a
noncomputable section
variable {K : Type u} [Field K]
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
section Decomp
variable (K V)
variable (B : Type u) [CommRing B] [Algebra K B]
variable {K V B}

Lean source · statement

theorem red_includeRight (b : B) :
    red K V B (Algebra.TensorProduct.includeRight (R := K) (A := TrivSqZeroExt K V) b) = b

theorem

σ_includeRight

L87 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit.P2mTJ2a.σ_includeRight

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit
open scoped TensorProduct
open TrivSqZeroExt
universe u
namespace P2mTJ2a
noncomputable section
variable {K : Type u} [Field K]
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
section Decomp
variable (K V)
variable (B : Type u) [CommRing B] [Algebra K B]
variable {K V B}

Lean source · statement

theorem σ_includeRight (b : B) :
    σ K V B (Algebra.TensorProduct.includeRight (R := K) (A := TrivSqZeroExt K V) b) = 0

theorem

σ_one

L92 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit.P2mTJ2a.σ_one

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit
open scoped TensorProduct
open TrivSqZeroExt
universe u
namespace P2mTJ2a
noncomputable section
variable {K : Type u} [Field K]
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
section Decomp
variable (K V)
variable (B : Type u) [CommRing B] [Algebra K B]
variable {K V B}
omit [IsCentralScalar K V] in

Lean source · statement

theorem σ_one : σ K V B 1 = 0

theorem

includeRight_red_add_incl_σ

L95 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit.P2mTJ2a.includeRight_red_add_incl_σ

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit
open scoped TensorProduct
open TrivSqZeroExt
universe u
namespace P2mTJ2a
noncomputable section
variable {K : Type u} [Field K]
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
section Decomp
variable (K V)
variable (B : Type u) [CommRing B] [Algebra K B]
variable {K V B}

Lean source · statement

theorem includeRight_red_add_incl_σ (z : TrivSqZeroExt K V ⊗[K] B) :
    Algebra.TensorProduct.includeRight (red K V B z) + incl K V B (σ K V B z) = z

theorem

eq_one_add_incl_of_red_eq_one

L109 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit.P2mTJ2a.eq_one_add_incl_of_red_eq_one

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit
open scoped TensorProduct
open TrivSqZeroExt
universe u
namespace P2mTJ2a
noncomputable section
variable {K : Type u} [Field K]
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
section Decomp
variable (K V)
variable (B : Type u) [CommRing B] [Algebra K B]
variable {K V B}

Lean source · statement

theorem eq_one_add_incl_of_red_eq_one {z : TrivSqZeroExt K V ⊗[K] B} (hz : red K V B z = 1) :
    z = 1 + incl K V B (σ K V B z)

theorem

incl_mul_incl

L113 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit.P2mTJ2a.incl_mul_incl

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit
open scoped TensorProduct
open TrivSqZeroExt
universe u
namespace P2mTJ2a
noncomputable section
variable {K : Type u} [Field K]
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
section Decomp
variable (K V)
variable (B : Type u) [CommRing B] [Algebra K B]
variable {K V B}

Lean source · statement

theorem incl_mul_incl (w w' : B ⊗[K] V) : incl K V B w * incl K V B w' = 0

theorem

includeRight_mul_incl

L123 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit.P2mTJ2a.includeRight_mul_incl

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit
open scoped TensorProduct
open TrivSqZeroExt
universe u
namespace P2mTJ2a
noncomputable section
variable {K : Type u} [Field K]
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
section Decomp
variable (K V)
variable (B : Type u) [CommRing B] [Algebra K B]
variable {K V B}

Lean source · statement

theorem includeRight_mul_incl (b : B) (w : B ⊗[K] V) :
    Algebra.TensorProduct.includeRight (R := K) (A := TrivSqZeroExt K V) b * incl K V B w = incl
      K V B (b • w)

def

unitOf

L134 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit.P2mTJ2a.unitOf

Documentation

The unit 1 + w whose inverse is 1 - w in the square-zero extension.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit
open scoped TensorProduct
open TrivSqZeroExt
universe u
namespace P2mTJ2a
noncomputable section
variable {K : Type u} [Field K]
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
section Decomp
variable (K V)
variable (B : Type u) [CommRing B] [Algebra K B]
variable {K V B}

Lean source · full declaration

def unitOf (w : B ⊗[K] V) : (TrivSqZeroExt K V ⊗[K] B)ˣ where
  val := 1 + incl K V B w
  inv := 1 - incl K V B w
  val_inv := by rw [add_mul, mul_sub, mul_sub, one_mul, mul_one, one_mul, incl_mul_incl]; abel
  inv_val := by rw [sub_mul, mul_add, mul_add, one_mul, mul_one, one_mul, incl_mul_incl]; abel

theorem

unitOf_val

L140 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit.P2mTJ2a.unitOf_val

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit
open scoped TensorProduct
open TrivSqZeroExt
universe u
namespace P2mTJ2a
noncomputable section
variable {K : Type u} [Field K]
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
section Decomp
variable (K V)
variable (B : Type u) [CommRing B] [Algebra K B]
variable {K V B}

Lean source · statement

theorem unitOf_val (w : B ⊗[K] V) : (unitOf w : TrivSqZeroExt K V ⊗[K] B) = 1 +
  incl K V B w

theorem

unitOf_inv_val

L142 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit.P2mTJ2a.unitOf_inv_val

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit
open scoped TensorProduct
open TrivSqZeroExt
universe u
namespace P2mTJ2a
noncomputable section
variable {K : Type u} [Field K]
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
section Decomp
variable (K V)
variable (B : Type u) [CommRing B] [Algebra K B]
variable {K V B}

Lean source · statement

theorem unitOf_inv_val (w : B ⊗[K] V) : (↑(unitOf w)⁻¹ : TrivSqZeroExt K V ⊗[K]
  B) = 1 - incl K V B w

theorem

one_add_incl_mul

L146 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit.P2mTJ2a.one_add_incl_mul

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit
open scoped TensorProduct
open TrivSqZeroExt
universe u
namespace P2mTJ2a
noncomputable section
variable {K : Type u} [Field K]
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
section Decomp
variable (K V)
variable (B : Type u) [CommRing B] [Algebra K B]
variable {K V B}

Lean source · statement

theorem one_add_incl_mul (w w' : B ⊗[K] V) :
    (1 + incl K V B w) * (1 + incl K V B w') = 1 + incl K V B (w + w')

theorem

red_unitOf

L150 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit.P2mTJ2a.red_unitOf

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit
open scoped TensorProduct
open TrivSqZeroExt
universe u
namespace P2mTJ2a
noncomputable section
variable {K : Type u} [Field K]
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
section Decomp
variable (K V)
variable (B : Type u) [CommRing B] [Algebra K B]
variable {K V B}

Lean source · statement

theorem red_unitOf (w : B ⊗[K] V) : red K V B ((unitOf w : (TrivSqZeroExt K V ⊗[K] B)ˣ) :
  TrivSqZeroExt K V ⊗[K] B) = 1

theorem

σ_unitOf

L154 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit.P2mTJ2a.σ_unitOf

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit
open scoped TensorProduct
open TrivSqZeroExt
universe u
namespace P2mTJ2a
noncomputable section
variable {K : Type u} [Field K]
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
section Decomp
variable (K V)
variable (B : Type u) [CommRing B] [Algebra K B]
variable {K V B}

Lean source · statement

theorem σ_unitOf (w : B ⊗[K] V) : σ K V B ((unitOf w : (TrivSqZeroExt K V ⊗[K] B)ˣ) :
  TrivSqZeroExt K V ⊗[K] B) = w

theorem

unit_eq

L158 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit.P2mTJ2a.unit_eq

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit
open scoped TensorProduct
open TrivSqZeroExt
universe u
namespace P2mTJ2a
noncomputable section
variable {K : Type u} [Field K]
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
section Decomp
variable (K V)
variable (B : Type u) [CommRing B] [Algebra K B]
variable {K V B}

Lean source · statement

theorem unit_eq (a : (TrivSqZeroExt K V ⊗[K] B)ˣ) :
    (a : TrivSqZeroExt K V ⊗[K] B) =
      Algebra.TensorProduct.includeRight (R := K) (A := TrivSqZeroExt K V)
          ((Units.map (red K V B : TrivSqZeroExt K V ⊗[K] B →* B) a : Bˣ) : B) *
        (1 + incl K V B (σ K V B ((a : TrivSqZeroExt K V ⊗[K] B) *
          Algebra.TensorProduct.includeRight (R := K) (A := TrivSqZeroExt K V)
          ((↑(Units.map (red K V B : TrivSqZeroExt K V ⊗[K] B →* B) a)⁻¹ : Bˣ) : B))))

theorem

unit_inv_eq

L174 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit.P2mTJ2a.unit_inv_eq

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit
open scoped TensorProduct
open TrivSqZeroExt
universe u
namespace P2mTJ2a
noncomputable section
variable {K : Type u} [Field K]
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
section Decomp
variable (K V)
variable (B : Type u) [CommRing B] [Algebra K B]
variable {K V B}

Lean source · statement

theorem unit_inv_eq (a : (TrivSqZeroExt K V ⊗[K] B)ˣ) :
    (↑a⁻¹ : TrivSqZeroExt K V ⊗[K] B) =
      Algebra.TensorProduct.includeRight (R := K) (A := TrivSqZeroExt K V)
          ((↑(Units.map (red K V B : TrivSqZeroExt K V ⊗[K] B →* B) a)⁻¹ : Bˣ) : B) *
        (1 - incl K V B (σ K V B ((a : TrivSqZeroExt K V ⊗[K] B) *
          Algebra.TensorProduct.includeRight (R := K) (A := TrivSqZeroExt K V)
          ((↑(Units.map (red K V B : TrivSqZeroExt K V ⊗[K] B →* B) a)⁻¹ : Bˣ) : B))))

theorem

map_incl

L198 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit.P2mTJ2a.map_incl

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit
open scoped TensorProduct
open TrivSqZeroExt
universe u
namespace P2mTJ2a
noncomputable section
variable {K : Type u} [Field K]
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
section Decomp
variable (K V)
variable (B : Type u) [CommRing B] [Algebra K B]
variable {K V B}
variable {C : Type u} [CommRing C] [Algebra K C] (ρ : B →ₐ[K] C)

Lean source · statement

theorem map_incl (w : B ⊗[K] V) :
    Algebra.TensorProduct.map (AlgHom.id K (TrivSqZeroExt K V)) ρ (incl K V B w) = incl K V C
      (ρ.toLinearMap.rTensor V w)

theorem

red_map

L205 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit.P2mTJ2a.red_map

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit
open scoped TensorProduct
open TrivSqZeroExt
universe u
namespace P2mTJ2a
noncomputable section
variable {K : Type u} [Field K]
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
section Decomp
variable (K V)
variable (B : Type u) [CommRing B] [Algebra K B]
variable {K V B}
variable {C : Type u} [CommRing C] [Algebra K C] (ρ : B →ₐ[K] C)

Lean source · statement

theorem red_map (z : TrivSqZeroExt K V ⊗[K] B) :
    red K V C (Algebra.TensorProduct.map (AlgHom.id K (TrivSqZeroExt K V)) ρ z) = ρ (red K V B
      z)

theorem

σ_map

L212 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit.P2mTJ2a.σ_map

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit
open scoped TensorProduct
open TrivSqZeroExt
universe u
namespace P2mTJ2a
noncomputable section
variable {K : Type u} [Field K]
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
section Decomp
variable (K V)
variable (B : Type u) [CommRing B] [Algebra K B]
variable {K V B}
variable {C : Type u} [CommRing C] [Algebra K C] (ρ : B →ₐ[K] C)

Lean source · statement

theorem σ_map (z : TrivSqZeroExt K V ⊗[K] B) :
    σ K V C (Algebra.TensorProduct.map (AlgHom.id K (TrivSqZeroExt K V)) ρ z) =
      ρ.toLinearMap.rTensor V (σ K V B z)

theorem

map_includeRight

L219 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit.P2mTJ2a.map_includeRight

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit
open scoped TensorProduct
open TrivSqZeroExt
universe u
namespace P2mTJ2a
noncomputable section
variable {K : Type u} [Field K]
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
section Decomp
variable (K V)
variable (B : Type u) [CommRing B] [Algebra K B]
variable {K V B}
variable {C : Type u} [CommRing C] [Algebra K C] (ρ : B →ₐ[K] C)

Lean source · statement

theorem map_includeRight (b : B) :
    Algebra.TensorProduct.map (AlgHom.id K (TrivSqZeroExt K V)) ρ
      (Algebra.TensorProduct.includeRight b) =
      Algebra.TensorProduct.includeRight (ρ b)

theorem

mkQ_ρ0

L231 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit.P2mTJ2a.mkQ_ρ0

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit
open scoped TensorProduct
open TrivSqZeroExt
universe u
namespace P2mTJ2a
noncomputable section
variable {K : Type u} [Field K]
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
section Cech
variable (𝒰 : TwoChartCech.Cover.{u, u} K) (V)

Lean source · statement

theorem mkQ_ρ0 (b : 𝒰.A0) : (LinearMap.range 𝒰.structureSheaf.cechDiff).mkQ (𝒰.ρ0 b) = 0

theorem

mkQ_ρ1

L237 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit.P2mTJ2a.mkQ_ρ1

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit
open scoped TensorProduct
open TrivSqZeroExt
universe u
namespace P2mTJ2a
noncomputable section
variable {K : Type u} [Field K]
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
section Cech
variable (𝒰 : TwoChartCech.Cover.{u, u} K) (V)

Lean source · statement

theorem mkQ_ρ1 (b : 𝒰.A1) : (LinearMap.range 𝒰.structureSheaf.cechDiff).mkQ (𝒰.ρ1 b) = 0

theorem

rTensor_mkQ_rTensor_ρ0

L244 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit.P2mTJ2a.rTensor_mkQ_rTensor_ρ0

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit
open scoped TensorProduct
open TrivSqZeroExt
universe u
namespace P2mTJ2a
noncomputable section
variable {K : Type u} [Field K]
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
section Cech
variable (𝒰 : TwoChartCech.Cover.{u, u} K) (V)
omit [Module Kᵐᵒᵖ V] [IsCentralScalar K V] in

Lean source · statement

theorem rTensor_mkQ_rTensor_ρ0 (β : 𝒰.A0 ⊗[K] V) :
    (LinearMap.range 𝒰.structureSheaf.cechDiff).mkQ.rTensor V (𝒰.ρ0.toLinearMap.rTensor V β) = 0

theorem

rTensor_mkQ_rTensor_ρ1

L253 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit.P2mTJ2a.rTensor_mkQ_rTensor_ρ1

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit
open scoped TensorProduct
open TrivSqZeroExt
universe u
namespace P2mTJ2a
noncomputable section
variable {K : Type u} [Field K]
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
section Cech
variable (𝒰 : TwoChartCech.Cover.{u, u} K) (V)
omit [Module Kᵐᵒᵖ V] [IsCentralScalar K V] in

Lean source · statement

theorem rTensor_mkQ_rTensor_ρ1 (β : 𝒰.A1 ⊗[K] V) :
    (LinearMap.range 𝒰.structureSheaf.cechDiff).mkQ.rTensor V (𝒰.ρ1.toLinearMap.rTensor V β) = 0

theorem

exists_of_rTensor_mkQ_eq_zero

L262 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit.P2mTJ2a.exists_of_rTensor_mkQ_eq_zero

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit
open scoped TensorProduct
open TrivSqZeroExt
universe u
namespace P2mTJ2a
noncomputable section
variable {K : Type u} [Field K]
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
section Cech
variable (𝒰 : TwoChartCech.Cover.{u, u} K) (V)
omit [Module Kᵐᵒᵖ V] [IsCentralScalar K V] in

Lean source · statement

theorem exists_of_rTensor_mkQ_eq_zero {y : 𝒰.A01 ⊗[K] V}
    (hy : (LinearMap.range 𝒰.structureSheaf.cechDiff).mkQ.rTensor V y = 0) :
    ∃ (β0 : 𝒰.A0 ⊗[K] V) (β1 : 𝒰.A1 ⊗[K] V),
      y = 𝒰.ρ1.toLinearMap.rTensor V β1 - 𝒰.ρ0.toLinearMap.rTensor V β0

theorem

squareZeroUnit_cohomologous_iff_and_exists

L296 ↗

TwoChartCech.Cover.squareZeroUnit_cohomologous_iff_and_exists

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCoverSquareZeroUnit
open scoped TensorProduct
open TrivSqZeroExt
universe u
open P2mTJ2a in

Lean source · full declaration

theorem _root_.TwoChartCech.Cover.squareZeroUnit_cohomologous_iff_and_exists
    {K : Type u} [Field K] (𝒰 : TwoChartCech.Cover.{u, u} K)
    (V : Type u) [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V] :
    (∀ t t' : (TrivSqZeroExt K V ⊗[K] 𝒰.A01)ˣ,
      Algebra.TensorProduct.lift ((Algebra.ofId K 𝒰.A01).comp (TrivSqZeroExt.fstHom K K V))
        (AlgHom.id K 𝒰.A01)
          (fun _ _ => Commute.all _ _) (t : TrivSqZeroExt K V ⊗[K] 𝒰.A01) = 1 →
      Algebra.TensorProduct.lift ((Algebra.ofId K 𝒰.A01).comp (TrivSqZeroExt.fstHom K K V))
        (AlgHom.id K 𝒰.A01)
          (fun _ _ => Commute.all _ _) (t' : TrivSqZeroExt K V ⊗[K] 𝒰.A01) = 1 →
      ((∃ (a0 : (TrivSqZeroExt K V ⊗[K] 𝒰.A0)ˣ) (a1 : (TrivSqZeroExt K V ⊗[K] 𝒰.A1)ˣ),
          (t' : TrivSqZeroExt K V ⊗[K] 𝒰.A01) =
            Algebra.TensorProduct.map (AlgHom.id K (TrivSqZeroExt K V)) 𝒰.ρ0 (a0 : TrivSqZeroExt
              K V ⊗[K] 𝒰.A0) *
              (t : TrivSqZeroExt K V ⊗[K] 𝒰.A01) *
            Algebra.TensorProduct.map (AlgHom.id K (TrivSqZeroExt K V)) 𝒰.ρ1
              ((↑a1⁻¹ : (TrivSqZeroExt K V ⊗[K] 𝒰.A1)ˣ) : TrivSqZeroExt K V ⊗[K] 𝒰.A1)) ↔
        (LinearMap.range 𝒰.structureSheaf.cechDiff).mkQ.rTensor V
            ((TensorProduct.comm K V 𝒰.A01).toLinearMap
              (TensorProduct.map (TrivSqZeroExt.sndHom K V) LinearMap.id (t : TrivSqZeroExt K V
                ⊗[K] 𝒰.A01))) =
          (LinearMap.range 𝒰.structureSheaf.cechDiff).mkQ.rTensor V
            ((TensorProduct.comm K V 𝒰.A01).toLinearMap
              (TensorProduct.map (TrivSqZeroExt.sndHom K V) LinearMap.id (t' : TrivSqZeroExt K V
                ⊗[K] 𝒰.A01))))) ∧
    (∀ y : 𝒰.structureSheaf.H1 ⊗[K] V, ∃ t : (TrivSqZeroExt K V ⊗[K] 𝒰.A01)ˣ,
      Algebra.TensorProduct.lift ((Algebra.ofId K 𝒰.A01).comp (TrivSqZeroExt.fstHom K K V))
        (AlgHom.id K 𝒰.A01)
          (fun _ _ => Commute.all _ _) (t : TrivSqZeroExt K V ⊗[K] 𝒰.A01) = 1 ∧
      (LinearMap.range 𝒰.structureSheaf.cechDiff).mkQ.rTensor V
          ((TensorProduct.comm K V 𝒰.A01).toLinearMap
            (TensorProduct.map (TrivSqZeroExt.sndHom K V) LinearMap.id (t : TrivSqZeroExt K V
              ⊗[K] 𝒰.A01))) = y) := by
  change (∀ t t' : (TrivSqZeroExt K V ⊗[K] 𝒰.A01)ˣ, red K V 𝒰.A01 t = 1 → red K V 𝒰.A01 t' = 1 →
      ((∃ (a0 : (TrivSqZeroExt K V ⊗[K] 𝒰.A0)ˣ) (a1 : (TrivSqZeroExt K V ⊗[K] 𝒰.A1)ˣ),
          (t' : TrivSqZeroExt K V ⊗[K] 𝒰.A01) =
            Algebra.TensorProduct.map (AlgHom.id K (TrivSqZeroExt K V)) 𝒰.ρ0 (a0 : TrivSqZeroExt
              K V ⊗[K] 𝒰.A0) *
              (t : TrivSqZeroExt K V ⊗[K] 𝒰.A01) *
            Algebra.TensorProduct.map (AlgHom.id K (TrivSqZeroExt K V)) 𝒰.ρ1
              ((↑a1⁻¹ : (TrivSqZeroExt K V ⊗[K] 𝒰.A1)ˣ) : TrivSqZeroExt K V ⊗[K] 𝒰.A1)) ↔
        (LinearMap.range 𝒰.structureSheaf.cechDiff).mkQ.rTensor V (σ K V 𝒰.A01 t) =
          (LinearMap.range 𝒰.structureSheaf.cechDiff).mkQ.rTensor V (σ K V 𝒰.A01 t'))) ∧
    (∀ y : 𝒰.structureSheaf.H1 ⊗[K] V, ∃ t : (TrivSqZeroExt K V ⊗[K] 𝒰.A01)ˣ,
      red K V 𝒰.A01 t = 1 ∧ (LinearMap.range 𝒰.structureSheaf.cechDiff).mkQ.rTensor V (σ K V
        𝒰.A01 t) = y)
  refine ⟨fun t t' ht ht' => ⟨?_, ?_⟩, fun y => ?_⟩
  · rintro ⟨a0, a1, h⟩
    set u0 : 𝒰.A0ˣ := Units.map (red K V 𝒰.A0 : TrivSqZeroExt K V ⊗[K] 𝒰.A0 →* 𝒰.A0) a0 with hu0
    set u1 : 𝒰.A1ˣ := Units.map (red K V 𝒰.A1 : TrivSqZeroExt K V ⊗[K] 𝒰.A1 →* 𝒰.A1) a1 with hu1
    set β0 := σ K V 𝒰.A0 ((a0 : TrivSqZeroExt K V ⊗[K] 𝒰.A0) *
      Algebra.TensorProduct.includeRight ((↑u0⁻¹ : 𝒰.A0ˣ) : 𝒰.A0)) with hβ0
    set β1 := σ K V 𝒰.A1 ((a1 : TrivSqZeroExt K V ⊗[K] 𝒰.A1) *
      Algebra.TensorProduct.includeRight ((↑u1⁻¹ : 𝒰.A1ˣ) : 𝒰.A1)) with hβ1
    have ha0 := unit_eq (V := V) a0
    have ha1 := unit_inv_eq (V := V) a1
    rw [← hu0, ← hβ0] at ha0
    rw [← hu1, ← hβ1] at ha1
    have hg : 𝒰.ρ0 (u0 : 𝒰.A0) = 𝒰.ρ1 (u1 : 𝒰.A1) := by
      have hred := congrArg (red K V 𝒰.A01) h
      rw [ht', map_mul, map_mul, ht, mul_one, red_map, red_map] at hred
      have e0 : red K V 𝒰.A0 (a0 : TrivSqZeroExt K V ⊗[K] 𝒰.A0) = (u0 : 𝒰.A0) := by rw [hu0]; rfl
      have e1 : red K V 𝒰.A1 ((↑a1⁻¹ : (TrivSqZeroExt K V ⊗[K] 𝒰.A1)ˣ) : TrivSqZeroExt K V ⊗[K]
        𝒰.A1) =
          ((↑u1⁻¹ : 𝒰.A1ˣ) : 𝒰.A1) := by rw [hu1]; rfl
      rw [e0, e1] at hred
      have := congrArg (· * 𝒰.ρ1 (u1 : 𝒰.A1)) hred
      simp only [one_mul, mul_assoc, ← map_mul, Units.inv_mul, map_one, mul_one] at this
      exact this.symm
    set w := σ K V 𝒰.A01 (t : TrivSqZeroExt K V ⊗[K] 𝒰.A01) with hw
    have ht1 : (t : TrivSqZeroExt K V ⊗[K] 𝒰.A01) = 1 + incl K V 𝒰.A01 w :=
      eq_one_add_incl_of_red_eq_one ht
    have key : (t' : TrivSqZeroExt K V ⊗[K] 𝒰.A01) =
        1 + incl K V 𝒰.A01 (w + 𝒰.ρ0.toLinearMap.rTensor V β0 - 𝒰.ρ1.toLinearMap.rTensor V β1) := by
      rw [h, ha0, ha1, map_mul, map_mul, map_includeRight, map_includeRight, map_add, map_sub,
        map_one, map_one,
        map_incl, map_incl, ht1]
      set g := 𝒰.ρ0 (u0 : 𝒰.A0)
      have hg' : 𝒰.ρ1 ((↑u1⁻¹ : 𝒰.A1ˣ) : 𝒰.A1) * g = 1 := by
        rw [hg, ← map_mul, Units.inv_mul, map_one]
      calc Algebra.TensorProduct.includeRight g * (1 + incl K V 𝒰.A01 (𝒰.ρ0.toLinearMap.rTensor
        V β0)) *
            (1 + incl K V 𝒰.A01 w) *
            (Algebra.TensorProduct.includeRight (𝒰.ρ1 ((↑u1⁻¹ : 𝒰.A1ˣ) : 𝒰.A1)) *
              (1 - incl K V 𝒰.A01 (𝒰.ρ1.toLinearMap.rTensor V β1)))
          = (Algebra.TensorProduct.includeRight (R := K) (A := TrivSqZeroExt K V) (𝒰.ρ1 ((↑u1⁻¹
            : 𝒰.A1ˣ) : 𝒰.A1)) *
              Algebra.TensorProduct.includeRight g) *
            ((1 + incl K V 𝒰.A01 (𝒰.ρ0.toLinearMap.rTensor V β0)) * (1 + incl K V 𝒰.A01 w) *
              (1 - incl K V 𝒰.A01 (𝒰.ρ1.toLinearMap.rTensor V β1))) := by ring
        _ = 1 + incl K V 𝒰.A01 (w + 𝒰.ρ0.toLinearMap.rTensor V β0 - 𝒰.ρ1.toLinearMap.rTensor V
          β1) := by
          rw [← map_mul, hg', map_one, one_mul, sub_eq_add_neg, ← map_neg, one_add_incl_mul,
            one_add_incl_mul]
          congr 2
          abel
    have hσ' : σ K V 𝒰.A01 t' = w + 𝒰.ρ0.toLinearMap.rTensor V β0 - 𝒰.ρ1.toLinearMap.rTensor V
      β1 := by
      rw [key, map_add, σ_one, σ_incl, zero_add]
    rw [hσ', map_sub, map_add, rTensor_mkQ_rTensor_ρ0, rTensor_mkQ_rTensor_ρ1, add_zero, sub_zero]
  · intro hcls
    have hdiff : (LinearMap.range 𝒰.structureSheaf.cechDiff).mkQ.rTensor V (σ K V 𝒰.A01 t' - σ K
      V 𝒰.A01 t) = 0 := by
      rw [map_sub, hcls, sub_self]
    obtain ⟨β0, β1, hβ⟩ := exists_of_rTensor_mkQ_eq_zero V 𝒰 hdiff
    refine ⟨unitOf (-β0), unitOf (-β1), ?_⟩
    rw [unitOf_val, unitOf_inv_val, map_add, map_sub, map_one, map_one, map_incl, map_incl,
      eq_one_add_incl_of_red_eq_one ht, eq_one_add_incl_of_red_eq_one ht', sub_eq_add_neg, ←
        map_neg,
      one_add_incl_mul, one_add_incl_mul, map_neg, map_neg, neg_neg]
    congr 2
    rw [sub_eq_iff_eq_add] at hβ
    rw [hβ]
    abel
  · obtain ⟨w, rfl⟩ := LinearMap.rTensor_surjective V (Submodule.mkQ_surjective _) y
    exact ⟨unitOf w, red_unitOf w, by rw [σ_unitOf]⟩

Module documentation

Two Chart Cech Cover square Zero Unit cohomologous iff and exists

Declarations