Module

Exists_bounded_two_cochain_of_local_coboundaries.lean

Nyll.AlgebraicCurves.Geometry.Exists_bounded_two_cochain_of_local_coboundaries

65 declarations indexed from sourceView source ↗

Module documentation

Exists bounded two cochain of local coboundaries

Imports25

Mathlib.Algebra.Field.Defs
Mathlib.Algebra.Ring.Defs
Mathlib.Algebra.Group.Action.Defs
Mathlib.Algebra.Group.Pi.Basic
Mathlib.Algebra.Group.TransferInstance
Mathlib.Algebra.Notation.Pi.Defs
Mathlib.Algebra.Notation.Pi.Basic
Mathlib.Algebra.Module.Pi
Mathlib.Algebra.Module.Submodule.Lattice
Mathlib.Algebra.BigOperators.Group.Finset.Defs
Mathlib.Algebra.BigOperators.Group.Finset.Basic
Mathlib.Algebra.BigOperators.Group.Finset.Sigma
Mathlib.Algebra.BigOperators.Ring.Finset
Mathlib.Algebra.Polynomial.Basic
Mathlib.Algebra.Polynomial.Degree.Defs
Mathlib.Algebra.Polynomial.Degree.Operations
Mathlib.Algebra.Polynomial.Degree.Domain
Mathlib.Algebra.Polynomial.BigOperators
Mathlib.Algebra.Polynomial.FieldDivision
Mathlib.Algebra.EuclideanDomain.Defs
Mathlib.RingTheory.Ideal.Defs
Mathlib.RingTheory.Ideal.Maximal
Mathlib.Tactic.SplitIfs
Mathlib.Tactic.Ring.RingNF
Mathlib.Tactic.LinearCombination

Imported by2

structure

Table

L58 ↗

AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries.PatchSol.Table

Documentation

Structure constants of a commutative unital multiplication table.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section TableAlgebra

Lean source · full declaration

structure Table (R : Type*) [CommRing R] (N : ℕ) where
  /-- The structure constants for multiplication in the indexed basis. -/
  γ : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → R
  /-- The zeroth basis vector acts as the multiplicative identity. -/
  unit : ∀ j k, γ 0 j k = if j = k then 1 else 0
  /-- The structure constants are symmetric in the two multiplicands. -/
  comm : ∀ i j k, γ i j k = γ j i k
  /-- The structure constants satisfy the associativity equations. -/
  assoc : ∀ i j l m, ∑ k, γ i j k * γ k l m = ∑ k, γ j l k * γ i k m

def

cst

L71 ↗

AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries.PatchSol.cst

Documentation

The product of coordinate vectors determined by structure constants.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}

Lean source · statement

def cst (γ : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → R) (x y : Fin (N + 1) → R) :
    Fin (N + 1) → R

theorem

cst_apply

L75 ↗

AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries.PatchSol.cst_apply

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}

Lean source · statement

theorem cst_apply (γ : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → R) (x y : Fin (N + 1) → R)
    (m : Fin (N + 1)) : cst γ x y m = ∑ i, ∑ j, x i * y j * γ i j m

theorem

sum3_rot

L78 ↗

AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries.PatchSol.sum3_rot

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}

Lean source · statement

theorem sum3_rot (f : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → R) :
    ∑ q, ∑ l, ∑ t, f q l t = ∑ l, ∑ t, ∑ q, f q l t

theorem

sum4_rot

L83 ↗

AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries.PatchSol.sum4_rot

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}

Lean source · statement

theorem sum4_rot (f : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → R) :
    ∑ q, ∑ t, ∑ k, ∑ l, f q t k l = ∑ k, ∑ l, ∑ t, ∑ q, f q t k l

theorem

cst_cst_left

L94 ↗

AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries.PatchSol.cst_cst_left

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}

Lean source · statement

theorem cst_cst_left (γo γi : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → R)
    (a b c : Fin (N + 1) → R) (s : Fin (N + 1)) :
    cst γo (cst γi a b) c s = ∑ k, ∑ l, ∑ t, a k * b l * c t * ∑ q, γi k l q * γo q t s

theorem

cst_cst_right

L103 ↗

AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries.PatchSol.cst_cst_right

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}

Lean source · statement

theorem cst_cst_right (γo γi : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → R)
    (a b c : Fin (N + 1) → R) (s : Fin (N + 1)) :
    cst γo a (cst γi b c) s = ∑ k, ∑ l, ∑ t, a k * b l * c t * ∑ q, γi l t q * γo k q s

theorem

cst_comm_of

L113 ↗

AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries.PatchSol.cst_comm_of

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}

Lean source · statement

theorem cst_comm_of (γ : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → R)
    (hc : ∀ i j k, γ i j k = γ j i k) (a b : Fin (N + 1) → R) : cst γ a b = cst γ b a

theorem

cst_add_left

L120 ↗

AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries.PatchSol.cst_add_left

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}

Lean source · statement

theorem cst_add_left (γ : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → R) (a a' b : Fin (N + 1) → R) :
    cst γ (a + a') b = cst γ a b + cst γ a' b

theorem

cst_add_right

L125 ↗

AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries.PatchSol.cst_add_right

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}

Lean source · statement

theorem cst_add_right (γ : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → R) (a b b' : Fin (N + 1) → R) :
    cst γ a (b + b') = cst γ a b + cst γ a b'

theorem

cst_smul_left

L130 ↗

AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries.PatchSol.cst_smul_left

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}

Lean source · statement

theorem cst_smul_left (γ : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → R) (z : R)
    (a b : Fin (N + 1) → R) : cst γ (z • a) b = z • cst γ a b

theorem

cst_zero_left

L135 ↗

AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries.PatchSol.cst_zero_left

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}

Lean source · statement

theorem cst_zero_left (γ : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → R) (b : Fin (N + 1) → R) :
    cst γ 0 b = 0

theorem

cst_unit_left

L139 ↗

AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries.PatchSol.cst_unit_left

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}

Lean source · full declaration

theorem cst_unit_left (γ : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → R)
    (h1 : ∀ j k, γ 0 j k = if j = k then 1 else 0) (b : Fin (N + 1) → R) :
    cst γ (Pi.single 0 1) b = b := by
  funext m
  rw [cst_apply, Finset.sum_eq_single 0]
  · simp only [Pi.single_eq_same, one_mul, h1]
    rw [Finset.sum_eq_single m]
    · simp
    · intro j _ hj; simp [hj]
    · intro h; exact absurd (Finset.mem_univ m) h
  · intro i _ hi; simp [Pi.single_eq_of_ne hi]
  · intro h; exact absurd (Finset.mem_univ (0 : Fin (N + 1))) h

structure

TAlg

L153 ↗

AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries.PatchSol.TAlg

Documentation

The algebra with the given multiplication table.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}

Lean source · full declaration

structure TAlg (T : Table R N) where
  /-- The coordinates of an algebra element in the indexed basis. -/
  coord : Fin (N + 1) → R

theorem

ext

L161 ↗

AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries.PatchSol.TAlg.ext

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
namespace TAlg
variable (T : Table R N)

Lean source · statement

theorem ext {x y : TAlg T} (h : x.coord = y.coord) : x = y

def

equiv

L165 ↗

AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries.PatchSol.TAlg.equiv

Documentation

The coordinate equivalence of the table algebra.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
namespace TAlg
variable (T : Table R N)

Lean source · full declaration

def equiv : TAlg T ≃ (Fin (N + 1) → R) where
  toFun := coord
  invFun := TAlg.mk
  left_inv _ := rfl
  right_inv _ := rfl

instance

(anonymous instance)

L171 ↗

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
namespace TAlg
variable (T : Table R N)

Lean source · statement

instance : AddCommGroup (TAlg T)

theorem

coord_add

L173 ↗

AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries.PatchSol.TAlg.coord_add

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
namespace TAlg
variable (T : Table R N)

Lean source · statement

theorem coord_add (x y : TAlg T) : (x + y).coord = x.coord + y.coord

theorem

coord_zero

L174 ↗

AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries.PatchSol.TAlg.coord_zero

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
namespace TAlg
variable (T : Table R N)

Lean source · statement

theorem coord_zero : (0 : TAlg T).coord = 0

theorem

coord_neg

L175 ↗

AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries.PatchSol.TAlg.coord_neg

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
namespace TAlg
variable (T : Table R N)

Lean source · statement

theorem coord_neg (x : TAlg T) : (-x).coord = -x.coord

theorem

coord_sub

L176 ↗

AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries.PatchSol.TAlg.coord_sub

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
namespace TAlg
variable (T : Table R N)

Lean source · statement

theorem coord_sub (x y : TAlg T) : (x - y).coord = x.coord - y.coord

theorem

coord_mk

L177 ↗

AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries.PatchSol.TAlg.coord_mk

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
namespace TAlg
variable (T : Table R N)

Lean source · statement

theorem coord_mk (v : Fin (N + 1) → R) : (TAlg.mk v : TAlg T).coord = v

instance

(anonymous instance)

L179 ↗

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
namespace TAlg
variable (T : Table R N)

Lean source · statement

instance : Mul (TAlg T)

instance

(anonymous instance)

L181 ↗

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
namespace TAlg
variable (T : Table R N)

Lean source · statement

instance : One (TAlg T)

theorem

coord_mul

L183 ↗

AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries.PatchSol.TAlg.coord_mul

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
namespace TAlg
variable (T : Table R N)

Lean source · statement

theorem coord_mul (x y : TAlg T) : (x * y).coord = cst T.γ x.coord y.coord

theorem

coord_one

L184 ↗

AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries.PatchSol.TAlg.coord_one

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
namespace TAlg
variable (T : Table R N)

Lean source · statement

theorem coord_one : (1 : TAlg T).coord = Pi.single 0 1

theorem

mul_comm'

L186 ↗

AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries.PatchSol.TAlg.mul_comm'

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
namespace TAlg
variable (T : Table R N)

Lean source · statement

theorem mul_comm' (x y : TAlg T) : x * y = y * x

theorem

mul_assoc'

L189 ↗

AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries.PatchSol.TAlg.mul_assoc'

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
namespace TAlg
variable (T : Table R N)

Lean source · statement

theorem mul_assoc' (x y z : TAlg T) : x * y * z = x * (y * z)

theorem

one_mul'

L198 ↗

AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries.PatchSol.TAlg.one_mul'

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
namespace TAlg
variable (T : Table R N)

Lean source · statement

theorem one_mul' (x : TAlg T) : 1 * x = x

instance

instCommRing

L201 ↗

AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries.PatchSol.TAlg.instCommRing

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
namespace TAlg
variable (T : Table R N)

Lean source · full declaration

instance instCommRing : CommRing (TAlg T) where
  __ := (inferInstance : AddCommGroup (TAlg T))
  mul := (· * ·)
  one := 1
  mul_assoc := mul_assoc' T
  one_mul := one_mul' T
  mul_one x := by rw [mul_comm']; exact one_mul' T x
  zero_mul x := by ext1; simp only [coord_mul, coord_zero]; exact cst_zero_left _ _
  mul_zero x := by rw [mul_comm']; ext1; simp only [coord_mul, coord_zero]; exact cst_zero_left _ _
  left_distrib x y z := by ext1; simp only [coord_mul, coord_add]; exact cst_add_right _ _ _ _
  right_distrib x y z := by ext1; simp only [coord_mul, coord_add]; exact cst_add_left _ _ _ _
  mul_comm := mul_comm' T

def

e

L215 ↗

AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries.PatchSol.TAlg.e

Documentation

The coordinate basis vector of the algebra defined by the multiplication table.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
namespace TAlg
variable (T : Table R N)

Lean source · statement

def e (i : Fin (N + 1)) : TAlg T

theorem

coord_e

L217 ↗

AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries.PatchSol.TAlg.coord_e

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
namespace TAlg
variable (T : Table R N)

Lean source · statement

theorem coord_e (i : Fin (N + 1)) : (e T i).coord = Pi.single i 1

def

D1

L225 ↗

AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries.PatchSol.D1

Documentation

The Hochschild coboundary of a linear cochain in coordinates given by the multiplication constants.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
open scoped TAlg

Lean source · statement

def D1 (γ : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → R) (lam : Fin (N + 1) → Fin (N + 1) → R)
    (i j m : Fin (N + 1)) : R

def

D2

L230 ↗

AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries.PatchSol.D2

Documentation

The Hochschild coboundary of a bilinear cochain in multiplication coordinates.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
open scoped TAlg

Lean source · statement

def D2 (γ : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → R)
    (φ : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → R) (i j l m : Fin (N + 1)) : R

def

L1

L240 ↗

AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries.PatchSol.L1

Documentation

The linear coordinate operation determined by the matrix of coefficients.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
open scoped TAlg
section Semantics
variable (T : Table R N)

Lean source · statement

def L1 (lam : Fin (N + 1) → Fin (N + 1) → R) (x : TAlg T) : TAlg T

def

L2

L244 ↗

AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries.PatchSol.L2

Documentation

The bilinear coordinate operation determined by the three-index array of coefficients.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
open scoped TAlg
section Semantics
variable (T : Table R N)

Lean source · statement

def L2 (φ : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → R) (x y : TAlg T) : TAlg T

def

hd1

L248 ↗

AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries.PatchSol.hd1

Documentation

The Hochschild coboundary of the specified linear coordinate operation.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
open scoped TAlg
section Semantics
variable (T : Table R N)

Lean source · statement

def hd1 (lam : Fin (N + 1) → Fin (N + 1) → R) (x y : TAlg T) : TAlg T

def

hd2

L252 ↗

AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries.PatchSol.hd2

Documentation

The Hochschild coboundary of a bilinear operation on the algebra.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
open scoped TAlg
section Semantics
variable (T : Table R N)

Lean source · statement

def hd2 (Φ : TAlg T → TAlg T → TAlg T) (x y z : TAlg T) : TAlg T

theorem

coord_mul_L1

L255 ↗

AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries.PatchSol.coord_mul_L1

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
open scoped TAlg
section Semantics
variable (T : Table R N)

Lean source · statement

theorem coord_mul_L1 (lam : Fin (N + 1) → Fin (N + 1) → R) (x y : TAlg T) (m : Fin (N + 1)) :
    (x * L1 T lam y).coord m = ∑ i, ∑ j, x.coord i * y.coord j * ∑ q, lam j q * T.γ i q m

theorem

coord_L1_mul

L264 ↗

AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries.PatchSol.coord_L1_mul

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
open scoped TAlg
section Semantics
variable (T : Table R N)

Lean source · statement

theorem coord_L1_mul (lam : Fin (N + 1) → Fin (N + 1) → R) (x y : TAlg T) (m : Fin (N + 1)) :
    (L1 T lam (x * y)).coord m = ∑ i, ∑ j, x.coord i * y.coord j * ∑ q, T.γ i j q * lam q m

theorem

sum3_rot'

L272 ↗

AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries.PatchSol.sum3_rot'

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
open scoped TAlg
section Semantics
variable (T : Table R N)

Lean source · statement

theorem sum3_rot' (f : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → R) :
    ∑ q, ∑ j, ∑ i, f q j i = ∑ i, ∑ j, ∑ q, f q j i

theorem

coord_L1_mul'

L278 ↗

AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries.PatchSol.coord_L1_mul'

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
open scoped TAlg
section Semantics
variable (T : Table R N)

Lean source · statement

theorem coord_L1_mul' (lam : Fin (N + 1) → Fin (N + 1) → R) (x y : TAlg T) (m : Fin (N + 1)) :
    (L1 T lam x * y).coord m = ∑ i, ∑ j, x.coord i * y.coord j * ∑ q, lam i q * T.γ q j m

theorem

coord_hd1

L287 ↗

AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries.PatchSol.coord_hd1

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
open scoped TAlg
section Semantics
variable (T : Table R N)

Lean source · statement

theorem coord_hd1 (lam : Fin (N + 1) → Fin (N + 1) → R) (x y : TAlg T) (m : Fin (N + 1)) :
    (hd1 T lam x y).coord m = ∑ i, ∑ j, x.coord i * y.coord j * D1 T.γ lam i j m

theorem

coord_hd2

L293 ↗

AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries.PatchSol.coord_hd2

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
open scoped TAlg
section Semantics
variable (T : Table R N)

Lean source · statement

theorem coord_hd2 (φ : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → R) (x y z : TAlg T)
    (s : Fin (N + 1)) :
    (hd2 T (L2 T φ) x y z).coord s =
      ∑ k, ∑ l, ∑ t, x.coord k * y.coord l * z.coord t * D2 T.γ φ k l t s

theorem

sum3_single

L301 ↗

AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries.PatchSol.sum3_single

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
open scoped TAlg
section Semantics
variable (T : Table R N)

Lean source · statement

theorem sum3_single (f : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → R) (i j l : Fin (N + 1)) :
    ∑ k, ∑ q, ∑ t, (Pi.single i 1 : Fin (N + 1) → R) k * (Pi.single j 1 : Fin (N + 1) → R) q *
      (Pi.single l 1 : Fin (N + 1) → R) t * f k q t = f i j l

theorem

sum2_single

L313 ↗

AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries.PatchSol.sum2_single

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
open scoped TAlg
section Semantics
variable (T : Table R N)

Lean source · statement

theorem sum2_single (f : Fin (N + 1) → Fin (N + 1) → R) (i j : Fin (N + 1)) :
    ∑ k, ∑ q, (Pi.single i 1 : Fin (N + 1) → R) k * (Pi.single j 1 : Fin (N + 1) → R) q * f k q =
      f i j

theorem

L2_D1_eq_hd1

L323 ↗

AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries.PatchSol.L2_D1_eq_hd1

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
open scoped TAlg
section Semantics
variable (T : Table R N)

Lean source · statement

theorem L2_D1_eq_hd1 (lam : Fin (N + 1) → Fin (N + 1) → R) (y z : TAlg T) :
    L2 T (D1 T.γ lam) y z = hd1 T lam y z

theorem

hd2_hd1_eq_zero

L330 ↗

AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries.PatchSol.hd2_hd1_eq_zero

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
open scoped TAlg
section Semantics
variable (T : Table R N)

Lean source · statement

theorem hd2_hd1_eq_zero (lam : Fin (N + 1) → Fin (N + 1) → R) (x y z : TAlg T) :
    hd2 T (hd1 T lam) x y z = 0

theorem

D2_D1

L335 ↗

AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries.PatchSol.D2_D1

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
open scoped TAlg
section Semantics
variable (T : Table R N)

Lean source · statement

theorem D2_D1 (lam : Fin (N + 1) → Fin (N + 1) → R) (i j l m : Fin (N + 1)) :
    D2 T.γ (D1 T.γ lam) i j l m = 0

theorem

D2_add

L350 ↗

AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries.PatchSol.D2_add

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
open scoped TAlg
section Linear
variable (γ : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → R)

Lean source · statement

theorem D2_add (φ φ' : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → R) (i j l m : Fin (N + 1)) :
    D2 γ (φ + φ') i j l m = D2 γ φ i j l m + D2 γ φ' i j l m

theorem

D2_smul

L354 ↗

AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries.PatchSol.D2_smul

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
open scoped TAlg
section Linear
variable (γ : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → R)

Lean source · statement

theorem D2_smul (c : R) (φ : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → R) (i j l m : Fin (N + 1)) :
    D2 γ (c • φ) i j l m = c * D2 γ φ i j l m

theorem

D2_zero

L360 ↗

AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries.PatchSol.D2_zero

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
open scoped TAlg
section Linear
variable (γ : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → R)

Lean source · statement

theorem D2_zero (i j l m : Fin (N + 1)) :
    D2 γ (0 : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → R) i j l m = 0

theorem

D2_sub

L364 ↗

AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries.PatchSol.D2_sub

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
open scoped TAlg
section Linear
variable (γ : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → R)

Lean source · statement

theorem D2_sub (φ φ' : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → R) (i j l m : Fin (N + 1)) :
    D2 γ (φ - φ') i j l m = D2 γ φ i j l m - D2 γ φ' i j l m

theorem

D1_add

L368 ↗

AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries.PatchSol.D1_add

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
open scoped TAlg
section Linear
variable (γ : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → R)

Lean source · statement

theorem D1_add (lam lam' : Fin (N + 1) → Fin (N + 1) → R) (i j m : Fin (N + 1)) :
    D1 γ (lam + lam') i j m = D1 γ lam i j m + D1 γ lam' i j m

theorem

D1_smul

L372 ↗

AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries.PatchSol.D1_smul

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
open scoped TAlg
section Linear
variable (γ : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → R)

Lean source · statement

theorem D1_smul (c : R) (lam : Fin (N + 1) → Fin (N + 1) → R) (i j m : Fin (N + 1)) :
    D1 γ (c • lam) i j m = c * D1 γ lam i j m

theorem

D1_symm

L378 ↗

AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries.PatchSol.D1_symm

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
open scoped TAlg
section Linear
variable (γ : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → R)

Lean source · statement

theorem D1_symm (hγc : ∀ i j k, γ i j k = γ j i k) (lam : Fin (N + 1) → Fin (N + 1) → R)
    (i j m : Fin (N + 1)) : D1 γ lam i j m = D1 γ lam j i m

theorem

D1_norm

L389 ↗

AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries.PatchSol.D1_norm

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
open scoped TAlg
section Linear
variable (γ : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → R)

Lean source · full declaration

theorem D1_norm (hγ1 : ∀ j k, γ 0 j k = if j = k then 1 else 0)
    (lam : Fin (N + 1) → Fin (N + 1) → R) (hlam : ∀ m, lam 0 m = 0) (j m : Fin (N + 1)) :
    D1 γ lam 0 j m = 0 := by
  simp only [D1, hlam, zero_mul, Finset.sum_const_zero, add_zero, hγ1]
  rw [Finset.sum_eq_single m, Finset.sum_eq_single j]
  · simp
  · intro k _ hk; simp [Ne.symm hk]
  · intro h; exact absurd (Finset.mem_univ j) h
  · intro k _ hk; simp [hk]
  · intro h; exact absurd (Finset.mem_univ m) h

theorem

d_le_two

L414 ↗

AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries.PatchSol.d_le_two

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section Degrees
variable {K : Type u} [Field K] {n : ℕ} (d : Fin (n + 1) → ℕ)
  (hd0 : d 0 = 0) (hd : ∀ i, i ≠ 0 → d i = 1 ∨ d i = 2)
  (γ : Fin (n + 1) → Fin (n + 1) → Fin (n + 1) → K[X])
  (hγ1 : ∀ j k, γ 0 j k = if j = k then 1 else 0)
  (hγc : ∀ i j k, γ i j k = γ j i k)
  (hγd : ∀ i j k, i ≠ 0 → j ≠ 0 → (γ i j k).natDegree ≤ d i + d j - d k)
include hd0 hd in

Lean source · statement

theorem d_le_two (m : Fin (n + 1)) : d m ≤ 2

theorem

one_le_d

L419 ↗

AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries.PatchSol.one_le_d

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section Degrees
variable {K : Type u} [Field K] {n : ℕ} (d : Fin (n + 1) → ℕ)
  (hd0 : d 0 = 0) (hd : ∀ i, i ≠ 0 → d i = 1 ∨ d i = 2)
  (γ : Fin (n + 1) → Fin (n + 1) → Fin (n + 1) → K[X])
  (hγ1 : ∀ j k, γ 0 j k = if j = k then 1 else 0)
  (hγc : ∀ i j k, γ i j k = γ j i k)
  (hγd : ∀ i j k, i ≠ 0 → j ≠ 0 → (γ i j k).natDegree ≤ d i + d j - d k)
include hd in

Lean source · statement

theorem one_le_d (m : Fin (n + 1)) (hm : m ≠ 0) : 1 ≤ d m

theorem

natDegree_γ_zero_right

L422 ↗

AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries.PatchSol.natDegree_γ_zero_right

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section Degrees
variable {K : Type u} [Field K] {n : ℕ} (d : Fin (n + 1) → ℕ)
  (hd0 : d 0 = 0) (hd : ∀ i, i ≠ 0 → d i = 1 ∨ d i = 2)
  (γ : Fin (n + 1) → Fin (n + 1) → Fin (n + 1) → K[X])
  (hγ1 : ∀ j k, γ 0 j k = if j = k then 1 else 0)
  (hγc : ∀ i j k, γ i j k = γ j i k)
  (hγd : ∀ i j k, i ≠ 0 → j ≠ 0 → (γ i j k).natDegree ≤ d i + d j - d k)
include hγ1 hγc in

Lean source · statement

theorem natDegree_γ_zero_right (i m : Fin (n + 1)) : (γ i 0 m).natDegree = 0

theorem

natDegree_D1_le

L425 ↗

AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries.PatchSol.natDegree_D1_le

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section Degrees
variable {K : Type u} [Field K] {n : ℕ} (d : Fin (n + 1) → ℕ)
  (hd0 : d 0 = 0) (hd : ∀ i, i ≠ 0 → d i = 1 ∨ d i = 2)
  (γ : Fin (n + 1) → Fin (n + 1) → Fin (n + 1) → K[X])
  (hγ1 : ∀ j k, γ 0 j k = if j = k then 1 else 0)
  (hγc : ∀ i j k, γ i j k = γ j i k)
  (hγd : ∀ i j k, i ≠ 0 → j ≠ 0 → (γ i j k).natDegree ≤ d i + d j - d k)
include hd0 hd hγ1 hγc hγd in

Lean source · statement

theorem natDegree_D1_le (E : ℕ) (r : Fin (n + 1) → Fin (n + 1) → K[X]) (hr0 : ∀ m, r 0 m = 0)
    (hr : ∀ i m, r i m = 0 ∨ (r i m).natDegree + 1 ≤ E) (i j m : Fin (n + 1)) (hi : i ≠ 0)
    (hj : j ≠ 0) : (D1 γ r i j m).natDegree ≤ E + d i + d j - d m

def

multIdeal

L473 ↗

AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries.PatchSol.multIdeal

Documentation

The ideal of scalars making the prescribed three-cochain a normalized symmetric coboundary.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section Main
variable {K : Type u} [Field K] {n : ℕ}

Lean source · full declaration

def multIdeal (γ : Fin (n + 1) → Fin (n + 1) → Fin (n + 1) → K[X])
    (a : Fin (n + 1) → Fin (n + 1) → Fin (n + 1) → Fin (n + 1) → K[X]) : Ideal K[X] where
  carrier := {s | ∃ φ : Fin (n + 1) → Fin (n + 1) → Fin (n + 1) → K[X],
    (∀ j k, φ 0 j k = 0) ∧ (∀ i j k, φ i j k = φ j i k) ∧ ∀ i j l m, D2 γ φ i j l m = s * a i j l m}
  zero_mem' := ⟨0, fun _ _ => rfl, fun _ _ _ => rfl, fun i j l m => by rw [D2_zero, zero_mul]⟩
  add_mem' := by
    rintro s s' ⟨φ, h1, h2, h3⟩ ⟨φ', h1', h2', h3'⟩
    refine ⟨φ + φ', fun j k => by simp [h1, h1'], fun i j k => by
      simp only [Pi.add_apply, h2 i j k, h2' i j k], fun i j l m => ?_⟩
    rw [D2_add, h3, h3', add_mul]
  smul_mem' := by
    rintro c s ⟨φ, h1, h2, h3⟩
    refine ⟨c • φ, fun j k => by simp [h1], fun i j k => by
      simp only [Pi.smul_apply, h2 i j k], fun i j l m => ?_⟩
    rw [D2_smul, h3, smul_eq_mul, mul_assoc]

theorem

mem_multIdeal

L489 ↗

AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries.PatchSol.mem_multIdeal

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section Main
variable {K : Type u} [Field K] {n : ℕ}

Lean source · statement

theorem mem_multIdeal (γ : Fin (n + 1) → Fin (n + 1) → Fin (n + 1) → K[X])
    (a : Fin (n + 1) → Fin (n + 1) → Fin (n + 1) → Fin (n + 1) → K[X]) (s : K[X]) :
    s ∈ multIdeal γ a ↔ ∃ φ : Fin (n + 1) → Fin (n + 1) → Fin (n + 1) → K[X],
      (∀ j k, φ 0 j k = 0) ∧ (∀ i j k, φ i j k = φ j i k) ∧
        ∀ i j l m, D2 γ φ i j l m = s * a i j l m

theorem

main

L496 ↗

AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries.PatchSol.main

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
noncomputable section
namespace PatchSol
section Main
variable {K : Type u} [Field K] {n : ℕ}

Lean source · full declaration

theorem main (d : Fin (n + 1) → ℕ)
    (hd0 : d 0 = 0) (hd : ∀ i, i ≠ 0 → d i = 1 ∨ d i = 2)
    (γ : Fin (n + 1) → Fin (n + 1) → Fin (n + 1) → K[X])
    (hγ1 : ∀ j k, γ 0 j k = if j = k then 1 else 0)
    (hγc : ∀ i j k, γ i j k = γ j i k)
    (hγa : ∀ i j l m, ∑ k, γ i j k * γ k l m = ∑ k, γ j l k * γ i k m)
    (hγd : ∀ i j k, i ≠ 0 → j ≠ 0 → (γ i j k).natDegree ≤ d i + d j - d k)
    (a : Fin (n + 1) → Fin (n + 1) → Fin (n + 1) → Fin (n + 1) → K[X])
    (hloc : ∀ P : Ideal K[X], P.IsMaximal → ∃ s : K[X], s ∉ P ∧ s ∈ multIdeal γ a)
    (t : K[X]) (ht : t ≠ 0) (φi : Fin (n + 1) → Fin (n + 1) → Fin (n + 1) → K[X])
    (hφi1 : ∀ j k, φi 0 j k = 0) (hφic : ∀ i j k, φi i j k = φi j i k)
    (hφid : ∀ i j k, i ≠ 0 → j ≠ 0 → (φi i j k).natDegree ≤ t.natDegree + d i + d j - d k)
    (hφia : ∀ i j l m, D2 γ φi i j l m = t * a i j l m)
    (hgen : ∀ ψ : Fin (n + 1) → Fin (n + 1) → Fin (n + 1) → K[X],
      (∀ j k, ψ 0 j k = 0) → (∀ i j k, ψ i j k = ψ j i k) → (∀ i j l m, D2 γ ψ i j l m = 0) →
      ∃ u : K[X], u ≠ 0 ∧ ∃ lam : Fin (n + 1) → Fin (n + 1) → K[X], (∀ m, lam 0 m = 0) ∧
        ∀ i j m, u * ψ i j m = D1 γ lam i j m) :
    ∃ φ : Fin (n + 1) → Fin (n + 1) → Fin (n + 1) → K[X],
      (∀ j k, φ 0 j k = 0) ∧ (∀ i j k, φ i j k = φ j i k) ∧
      (∀ i j k, i ≠ 0 → j ≠ 0 → (φ i j k).natDegree ≤ d i + d j - d k) ∧
      ∀ i j l m, D2 γ φ i j l m = a i j l m := by
  let T : Table K[X] n := ⟨γ, hγ1, hγc, hγa⟩
  have htop : multIdeal γ a = ⊤ := by
    by_contra hne
    obtain ⟨P, hP, hle⟩ := Ideal.exists_le_maximal _ hne
    obtain ⟨s, hsP, hs⟩ := hloc P hP
    exact hsP (hle hs)
  have h1 : (1 : K[X]) ∈ multIdeal γ a := by rw [htop]; exact Submodule.mem_top
  obtain ⟨φ₀, hφ₀1, hφ₀c, hφ₀a⟩ := (mem_multIdeal γ a 1).1 h1
  simp only [one_mul] at hφ₀a
  let ψ : Fin (n + 1) → Fin (n + 1) → Fin (n + 1) → K[X] := t • φ₀ - φi
  have hψ1 : ∀ j k, ψ 0 j k = 0 := fun j k => by simp [ψ, hφ₀1, hφi1]
  have hψc : ∀ i j k, ψ i j k = ψ j i k := fun i j k => by
    simp only [ψ, Pi.sub_apply, Pi.smul_apply, hφ₀c i j k, hφic i j k]
  have hψa : ∀ i j l m, D2 γ ψ i j l m = 0 := fun i j l m => by
    change D2 γ (t • φ₀ - φi) i j l m = 0
    rw [D2_sub, D2_smul, hφ₀a, hφia, sub_self]
  obtain ⟨u, hu, lam, hlam0, hlam⟩ := hgen ψ hψ1 hψc hψa
  have hut : u * t ≠ 0 := mul_ne_zero hu ht
  let q : Fin (n + 1) → Fin (n + 1) → K[X] := fun i m => lam i m / (u * t)
  let r : Fin (n + 1) → Fin (n + 1) → K[X] := fun i m => lam i m % (u * t)
  have hqr : ∀ i m, lam i m = (u * t) * q i m + r i m := fun i m =>
    (EuclideanDomain.div_add_mod (lam i m) (u * t)).symm
  have hq0 : ∀ m, q 0 m = 0 := fun m => by simp [q, hlam0]
  have hr0 : ∀ m, r 0 m = 0 := fun m => by simp [r, hlam0]
  have hrdeg : ∀ i m, r i m = 0 ∨ (r i m).natDegree + 1 ≤ (u * t).natDegree := by
    intro i m
    by_cases h : r i m = 0
    · exact Or.inl h
    · right
      have hlt : (r i m).degree < (u * t).degree := EuclideanDomain.mod_lt (lam i m) hut
      have := Polynomial.natDegree_lt_natDegree h hlt
      omega
  let φ : Fin (n + 1) → Fin (n + 1) → Fin (n + 1) → K[X] := fun i j k => φ₀ i j k - D1 γ q i j k
  have hlamq : lam = (u * t) • q + r := by
    funext i m; simp only [Pi.add_apply, Pi.smul_apply, smul_eq_mul]; exact hqr i m
  have hkey : ∀ i j k, (u * t) * φ i j k = u * φi i j k + D1 γ r i j k := by
    intro i j k
    have e1 : u * ψ i j k = D1 γ lam i j k := hlam i j k
    have e2 : D1 γ lam i j k = (u * t) * D1 γ q i j k + D1 γ r i j k := by
      rw [hlamq, D1_add, D1_smul]
    have e3 : u * ψ i j k = u * (t * φ₀ i j k) - u * φi i j k := by
      simp only [ψ, Pi.sub_apply, Pi.smul_apply, smul_eq_mul, mul_sub]
    change (u * t) * (φ₀ i j k - D1 γ q i j k) = u * φi i j k + D1 γ r i j k
    have : (u * t) * φ₀ i j k = u * φi i j k + (u * t) * D1 γ q i j k + D1 γ r i j k := by
      linear_combination e1 + e2 - e3
    rw [mul_sub, this]; ring
  refine ⟨φ, fun j k => ?_, fun i j k => ?_, fun i j k hi hj => ?_, fun i j l m => ?_⟩
  · change φ₀ 0 j k - D1 γ q 0 j k = 0
    rw [hφ₀1, D1_norm γ hγ1 q hq0, sub_zero]
  · change φ₀ i j k - D1 γ q i j k = φ₀ j i k - D1 γ q j i k
    rw [hφ₀c i j k, D1_symm γ hγc q i j k]
  · have hR : ((u * t) * φ i j k).natDegree ≤ (u * t).natDegree + (d i + d j - d k) := by
      rw [hkey]
      refine (natDegree_add_le _ _).trans (max_le ?_ ?_)
      · refine natDegree_mul_le.trans ?_
        have := hφid i j k hi hj
        rw [natDegree_mul hu ht]
        omega
      · have := natDegree_D1_le d hd0 hd γ hγ1 hγc hγd (u * t).natDegree r hr0 hrdeg i j k hi hj
        omega
    by_cases hφ0 : φ i j k = 0
    · rw [hφ0, natDegree_zero]; exact Nat.zero_le _
    · rw [natDegree_mul hut hφ0] at hR
      omega
  · change D2 γ (fun i j k => φ₀ i j k - D1 γ q i j k) i j l m = a i j l m
    have : (fun i j k => φ₀ i j k - D1 γ q i j k) = φ₀ - D1 γ q := by
      funext i j k; rfl
    rw [this, D2_sub, hφ₀a, D2_D1 T q, sub_zero]

theorem

exists_bounded_two_cochain_of_local_coboundaries

L593 ↗

AlgebraicCurve.exists_bounded_two_cochain_of_local_coboundaries

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_bounded_two_cochain_of_local_coboundaries
open Polynomial
universe u
open PatchSol in

Lean source · full declaration

theorem _root_.AlgebraicCurve.exists_bounded_two_cochain_of_local_coboundaries
    (K : Type u) [Field K] (n : ℕ) (d : Fin (n + 1) → ℕ)
    (hd0 : d 0 = 0) (hd : ∀ i, i ≠ 0 → d i = 1 ∨ d i = 2)
    (γ : Fin (n + 1) → Fin (n + 1) → Fin (n + 1) → K[X])
    (hγ1 : ∀ j k, γ 0 j k = if j = k then 1 else 0)
    (hγc : ∀ i j k, γ i j k = γ j i k)
    (hγa : ∀ i j l m, ∑ k, γ i j k * γ k l m = ∑ k, γ j l k * γ i k m)
    (hγd : ∀ i j k, i ≠ 0 → j ≠ 0 → (γ i j k).natDegree ≤ d i + d j - d k)
    (a : Fin (n + 1) → Fin (n + 1) → Fin (n + 1) → Fin (n + 1) → K[X])
    (hloc : ∀ P : Ideal K[X], P.IsMaximal → ∃ s : K[X], s ∉ P ∧
      ∃ φ : Fin (n + 1) → Fin (n + 1) → Fin (n + 1) → K[X],
        (∀ j k, φ 0 j k = 0) ∧ (∀ i j k, φ i j k = φ j i k) ∧
        ∀ i j l m, (∑ k, φ j l k * γ i k m) - (∑ k, γ i j k * φ k l m) +
          (∑ k, γ j l k * φ i k m) - (∑ k, φ i j k * γ k l m) = s * a i j l m)
    (hinfty : ∃ t : K[X], t ≠ 0 ∧
      ∃ φ : Fin (n + 1) → Fin (n + 1) → Fin (n + 1) → K[X],
        (∀ j k, φ 0 j k = 0) ∧ (∀ i j k, φ i j k = φ j i k) ∧
        (∀ i j k, i ≠ 0 → j ≠ 0 → (φ i j k).natDegree ≤ t.natDegree + d i + d j - d k) ∧
        ∀ i j l m, (∑ k, φ j l k * γ i k m) - (∑ k, γ i j k * φ k l m) +
          (∑ k, γ j l k * φ i k m) - (∑ k, φ i j k * γ k l m) = t * a i j l m)
    (hgen : ∀ ψ : Fin (n + 1) → Fin (n + 1) → Fin (n + 1) → K[X],
      (∀ j k, ψ 0 j k = 0) → (∀ i j k, ψ i j k = ψ j i k) →
      (∀ i j l m, (∑ k, ψ j l k * γ i k m) - (∑ k, γ i j k * ψ k l m) +
          (∑ k, γ j l k * ψ i k m) - (∑ k, ψ i j k * γ k l m) = 0) →
      ∃ u : K[X], u ≠ 0 ∧ ∃ lam : Fin (n + 1) → Fin (n + 1) → K[X], (∀ m, lam 0 m = 0) ∧
        ∀ i j m, u * ψ i j m =
          (∑ k, lam j k * γ i k m) - (∑ k, γ i j k * lam k m) + (∑ k, lam i k * γ k j m)) :
    ∃ φ : Fin (n + 1) → Fin (n + 1) → Fin (n + 1) → K[X],
      (∀ j k, φ 0 j k = 0) ∧ (∀ i j k, φ i j k = φ j i k) ∧
      (∀ i j k, i ≠ 0 → j ≠ 0 → (φ i j k).natDegree ≤ d i + d j - d k) ∧
      ∀ i j l m, (∑ k, φ j l k * γ i k m) - (∑ k, γ i j k * φ k l m) +
        (∑ k, γ j l k * φ i k m) - (∑ k, φ i j k * γ k l m) = a i j l m := by
  obtain ⟨t, ht, φi, hφi1, hφic, hφid, hφia⟩ := hinfty
  have hloc' : ∀ P : Ideal K[X], P.IsMaximal → ∃ s : K[X], s ∉ P ∧ s ∈ multIdeal γ a := by
    intro P hP
    obtain ⟨s, hs, φ, h1, h2, h3⟩ := hloc P hP
    exact ⟨s, hs, φ, h1, h2, h3⟩
  exact main d hd0 hd γ hγ1 hγc hγa hγd a hloc' t ht φi hφi1 hφic hφid hφia hgen

Module documentation

Exists bounded two cochain of local coboundaries

Declarations