Module

Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero.lean

Nyll.AlgebraicCurves.Geometry.Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero

31 declarations indexed from sourceView source ↗

Module documentation

Exists mul eq hochschild coboundary of discr ne zero

Imports6

Mathlib.RingTheory.DedekindDomain.IntegralClosure
Mathlib.RingTheory.Localization.NormTrace
Mathlib.RingTheory.Etale.Field
Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Mathlib.RingTheory.Discriminant
Nyll.AlgebraicCurves.Foundations.Algebra.Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle

Imported by2

def

cst

L43 ↗

AlgebraicCurves.Geometry.Proofs.Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero.GenH2Sol.cst

Documentation

The product of coordinate vectors determined by structure constants.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero
open Polynomial
open scoped nonZeroDivisors
universe u v
noncomputable section
namespace GenH2Sol
section Coord
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

L47 ↗

AlgebraicCurves.Geometry.Proofs.Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero.GenH2Sol.cst_apply

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero
open Polynomial
open scoped nonZeroDivisors
universe u v
noncomputable section
namespace GenH2Sol
section Coord
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

L50 ↗

AlgebraicCurves.Geometry.Proofs.Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero.GenH2Sol.sum3_rot

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero
open Polynomial
open scoped nonZeroDivisors
universe u v
noncomputable section
namespace GenH2Sol
section Coord
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

L55 ↗

AlgebraicCurves.Geometry.Proofs.Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero.GenH2Sol.sum4_rot

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero
open Polynomial
open scoped nonZeroDivisors
universe u v
noncomputable section
namespace GenH2Sol
section Coord
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

L66 ↗

AlgebraicCurves.Geometry.Proofs.Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero.GenH2Sol.cst_cst_left

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero
open Polynomial
open scoped nonZeroDivisors
universe u v
noncomputable section
namespace GenH2Sol
section Coord
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

L75 ↗

AlgebraicCurves.Geometry.Proofs.Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero.GenH2Sol.cst_cst_right

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero
open Polynomial
open scoped nonZeroDivisors
universe u v
noncomputable section
namespace GenH2Sol
section Coord
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

L85 ↗

AlgebraicCurves.Geometry.Proofs.Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero.GenH2Sol.cst_comm_of

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero
open Polynomial
open scoped nonZeroDivisors
universe u v
noncomputable section
namespace GenH2Sol
section Coord
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_single_left

L92 ↗

AlgebraicCurves.Geometry.Proofs.Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero.GenH2Sol.cst_single_left

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero
open Polynomial
open scoped nonZeroDivisors
universe u v
noncomputable section
namespace GenH2Sol
section Coord
variable {R : Type*} [CommRing R] {N : ℕ}

Lean source · statement

theorem cst_single_left (γ : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → R) (i : Fin (N + 1))
    (y : Fin (N + 1) → R) (m : Fin (N + 1)) :
    cst γ (Pi.single i 1) y m = ∑ q, y q * γ i q m

theorem

cst_single_single

L100 ↗

AlgebraicCurves.Geometry.Proofs.Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero.GenH2Sol.cst_single_single

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero
open Polynomial
open scoped nonZeroDivisors
universe u v
noncomputable section
namespace GenH2Sol
section Coord
variable {R : Type*} [CommRing R] {N : ℕ}

Lean source · full declaration

theorem cst_single_single (γ : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → R) (i j : Fin (N + 1)) :
    cst γ (Pi.single i 1) (Pi.single j 1) = fun m => γ i j m := by
  funext m
  rw [cst_single_left, Finset.sum_eq_single j]
  · simp
  · intro b _ hb; simp [Pi.single_eq_of_ne hb]
  · intro h; exact absurd (Finset.mem_univ j) h

def

D1

L110 ↗

AlgebraicCurves.Geometry.Proofs.Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero.GenH2Sol.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_mul_eq_hochschild_coboundary_of_discr_ne_zero
open Polynomial
open scoped nonZeroDivisors
universe u v
noncomputable section
namespace GenH2Sol
section Coord
variable {R : Type*} [CommRing R] {N : ℕ}

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

L115 ↗

AlgebraicCurves.Geometry.Proofs.Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero.GenH2Sol.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_mul_eq_hochschild_coboundary_of_discr_ne_zero
open Polynomial
open scoped nonZeroDivisors
universe u v
noncomputable section
namespace GenH2Sol
section Coord
variable {R : Type*} [CommRing R] {N : ℕ}

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

theorem

D1_smul

L120 ↗

AlgebraicCurves.Geometry.Proofs.Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero.GenH2Sol.D1_smul

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero
open Polynomial
open scoped nonZeroDivisors
universe u v
noncomputable section
namespace GenH2Sol
section Coord
variable {R : Type*} [CommRing R] {N : ℕ}

Lean source · statement

theorem D1_smul (γ : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → R) (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_neg

L127 ↗

AlgebraicCurves.Geometry.Proofs.Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero.GenH2Sol.D1_neg

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero
open Polynomial
open scoped nonZeroDivisors
universe u v
noncomputable section
namespace GenH2Sol
section Coord
variable {R : Type*} [CommRing R] {N : ℕ}

Lean source · statement

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

theorem

D1_map

L133 ↗

AlgebraicCurves.Geometry.Proofs.Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero.GenH2Sol.D1_map

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero
open Polynomial
open scoped nonZeroDivisors
universe u v
noncomputable section
namespace GenH2Sol
section Coord
variable {R : Type*} [CommRing R] {N : ℕ}

Lean source · full declaration

theorem D1_map {R' : Type*} [CommRing R'] (f : R →+* R')
    (γ : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → R) (lam : Fin (N + 1) → Fin (N + 1) → R)
    (i j m : Fin (N + 1)) :
    f (D1 γ lam i j m) = D1 (fun i j k => f (γ i j k)) (fun i m => f (lam i m)) i j m := by
  simp only [D1, map_add, map_sub, map_sum, map_mul]

theorem

D2_map

L139 ↗

AlgebraicCurves.Geometry.Proofs.Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero.GenH2Sol.D2_map

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero
open Polynomial
open scoped nonZeroDivisors
universe u v
noncomputable section
namespace GenH2Sol
section Coord
variable {R : Type*} [CommRing R] {N : ℕ}

Lean source · full declaration

theorem D2_map {R' : Type*} [CommRing R'] (f : R →+* R')
    (γ : 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)) :
    f (D2 γ φ i j l m) = D2 (fun i j k => f (γ i j k)) (fun i j k => f (φ i j k)) i j l m := by
  simp only [D2, map_add, map_sub, map_sum, map_mul]

theorem

hd2_expand

L145 ↗

AlgebraicCurves.Geometry.Proofs.Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero.GenH2Sol.hd2_expand

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero
open Polynomial
open scoped nonZeroDivisors
universe u v
noncomputable section
namespace GenH2Sol
section Coord
variable {R : Type*} [CommRing R] {N : ℕ}

Lean source · statement

theorem hd2_expand (γ φ : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → R)
    (X Y Z : Fin (N + 1) → R) (s : Fin (N + 1)) :
    cst γ X (cst φ Y Z) s - cst φ (cst γ X Y) Z s + cst φ X (cst γ Y Z) s -
        cst γ (cst φ X Y) Z s =
      ∑ k, ∑ l, ∑ t, X k * Y l * Z t * D2 γ φ k l t s

theorem

repr_sum_smul

L162 ↗

AlgebraicCurves.Geometry.Proofs.Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero.GenH2Sol.repr_sum_smul

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero
open Polynomial
open scoped nonZeroDivisors
universe u v
noncomputable section
namespace GenH2Sol
section Based
variable {L : Type*} [Field L] {F : Type*} [CommRing F] [Algebra L F] {N : ℕ}
  (bF : Module.Basis (Fin (N + 1)) L F)
  (γL : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → L)
  (hγL : ∀ i j m, bF.repr (bF i * bF j) m = γL i j m)

Lean source · statement

theorem repr_sum_smul (c : Fin (N + 1) → L) (m : Fin (N + 1)) :
    bF.repr (∑ k, c k • bF k) m = c m

theorem

repr_basis_eq_single

L173 ↗

AlgebraicCurves.Geometry.Proofs.Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero.GenH2Sol.repr_basis_eq_single

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero
open Polynomial
open scoped nonZeroDivisors
universe u v
noncomputable section
namespace GenH2Sol
section Based
variable {L : Type*} [Field L] {F : Type*} [CommRing F] [Algebra L F] {N : ℕ}
  (bF : Module.Basis (Fin (N + 1)) L F)
  (γL : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → L)
  (hγL : ∀ i j m, bF.repr (bF i * bF j) m = γL i j m)

Lean source · full declaration

theorem repr_basis_eq_single (i : Fin (N + 1)) :
    (fun k => bF.repr (bF i) k) = (Pi.single i 1 : Fin (N + 1) → L) := by
  funext k
  rw [bF.repr_self, Finsupp.single_apply, Pi.single_apply]
  by_cases h : k = i
  · subst h; simp
  · rw [ite_eq_right (Ne.symm h), ite_eq_right h]

theorem

repr_mul

L181 ↗

AlgebraicCurves.Geometry.Proofs.Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero.GenH2Sol.repr_mul

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero
open Polynomial
open scoped nonZeroDivisors
universe u v
noncomputable section
namespace GenH2Sol
section Based
variable {L : Type*} [Field L] {F : Type*} [CommRing F] [Algebra L F] {N : ℕ}
  (bF : Module.Basis (Fin (N + 1)) L F)
  (γL : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → L)
  (hγL : ∀ i j m, bF.repr (bF i * bF j) m = γL i j m)
include hγL in

Lean source · full declaration

theorem repr_mul (x y : F) (m : Fin (N + 1)) :
    bF.repr (x * y) m = cst γL (fun i => bF.repr x i) (fun j => bF.repr y j) m := by
  have hx : x = ∑ i, bF.repr x i • bF i := (bF.sum_repr x).symm
  have hy : y = ∑ j, bF.repr y j • bF j := (bF.sum_repr y).symm
  conv_lhs => rw [hx, hy, Finset.sum_mul_sum]
  rw [map_sum, Finsupp.finsetSum_apply, cst_apply]
  refine Finset.sum_congr rfl fun i _ => ?_
  rw [map_sum, Finsupp.finsetSum_apply]
  refine Finset.sum_congr rfl fun j _ => ?_
  rw [smul_mul_smul_comm, map_smul, Finsupp.smul_apply, hγL, smul_eq_mul]

def

Ψf

L194 ↗

AlgebraicCurves.Geometry.Proofs.Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero.GenH2Sol.Ψf

Documentation

The bilinear operation obtained by evaluating the specified coefficients in the chosen basis.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero
open Polynomial
open scoped nonZeroDivisors
universe u v
noncomputable section
namespace GenH2Sol
section Based
variable {L : Type*} [Field L] {F : Type*} [CommRing F] [Algebra L F] {N : ℕ}
  (bF : Module.Basis (Fin (N + 1)) L F)
  (γL : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → L)
  (hγL : ∀ i j m, bF.repr (bF i * bF j) m = γL i j m)

Lean source · statement

def Ψf (ψL : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → L) (x y : F) : F

theorem

Ψf_repr

L199 ↗

AlgebraicCurves.Geometry.Proofs.Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero.GenH2Sol.Ψf_repr

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero
open Polynomial
open scoped nonZeroDivisors
universe u v
noncomputable section
namespace GenH2Sol
section Based
variable {L : Type*} [Field L] {F : Type*} [CommRing F] [Algebra L F] {N : ℕ}
  (bF : Module.Basis (Fin (N + 1)) L F)
  (γL : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → L)
  (hγL : ∀ i j m, bF.repr (bF i * bF j) m = γL i j m)
variable (ψL : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → L)

Lean source · full declaration

theorem Ψf_repr (x y : F) (m : Fin (N + 1)) :
    bF.repr (Ψf bF ψL x y) m = cst ψL (fun i => bF.repr x i) (fun j => bF.repr y j) m :=
  repr_sum_smul bF _ m

theorem

Ψf_add_left

L203 ↗

AlgebraicCurves.Geometry.Proofs.Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero.GenH2Sol.Ψf_add_left

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero
open Polynomial
open scoped nonZeroDivisors
universe u v
noncomputable section
namespace GenH2Sol
section Based
variable {L : Type*} [Field L] {F : Type*} [CommRing F] [Algebra L F] {N : ℕ}
  (bF : Module.Basis (Fin (N + 1)) L F)
  (γL : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → L)
  (hγL : ∀ i j m, bF.repr (bF i * bF j) m = γL i j m)
variable (ψL : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → L)

Lean source · statement

theorem Ψf_add_left (x₁ x₂ y : F) : Ψf bF ψL (x₁ + x₂) y = Ψf bF ψL x₁ y + Ψf bF ψL x₂ y

theorem

Ψf_smul_left

L211 ↗

AlgebraicCurves.Geometry.Proofs.Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero.GenH2Sol.Ψf_smul_left

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero
open Polynomial
open scoped nonZeroDivisors
universe u v
noncomputable section
namespace GenH2Sol
section Based
variable {L : Type*} [Field L] {F : Type*} [CommRing F] [Algebra L F] {N : ℕ}
  (bF : Module.Basis (Fin (N + 1)) L F)
  (γL : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → L)
  (hγL : ∀ i j m, bF.repr (bF i * bF j) m = γL i j m)
variable (ψL : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → L)

Lean source · statement

theorem Ψf_smul_left (c : L) (x y : F) : Ψf bF ψL (c • x) y = c • Ψf bF ψL x y

theorem

Ψf_symm

L219 ↗

AlgebraicCurves.Geometry.Proofs.Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero.GenH2Sol.Ψf_symm

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero
open Polynomial
open scoped nonZeroDivisors
universe u v
noncomputable section
namespace GenH2Sol
section Based
variable {L : Type*} [Field L] {F : Type*} [CommRing F] [Algebra L F] {N : ℕ}
  (bF : Module.Basis (Fin (N + 1)) L F)
  (γL : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → L)
  (hγL : ∀ i j m, bF.repr (bF i * bF j) m = γL i j m)
variable (ψL : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → L)

Lean source · statement

theorem Ψf_symm (hψLc : ∀ i j k, ψL i j k = ψL j i k) (x y : F) :
    Ψf bF ψL x y = Ψf bF ψL y x

def

ΨL

L225 ↗

AlgebraicCurves.Geometry.Proofs.Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero.GenH2Sol.ΨL

Documentation

The symmetric bilinear map determined by the specified coefficients and basis.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero
open Polynomial
open scoped nonZeroDivisors
universe u v
noncomputable section
namespace GenH2Sol
section Based
variable {L : Type*} [Field L] {F : Type*} [CommRing F] [Algebra L F] {N : ℕ}
  (bF : Module.Basis (Fin (N + 1)) L F)
  (γL : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → L)
  (hγL : ∀ i j m, bF.repr (bF i * bF j) m = γL i j m)
variable (ψL : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → L)

Lean source · statement

def ΨL (hψLc : ∀ i j k, ψL i j k = ψL j i k) : F →ₗ[L] F →ₗ[L] F

theorem

ΨL_apply

L231 ↗

AlgebraicCurves.Geometry.Proofs.Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero.GenH2Sol.ΨL_apply

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero
open Polynomial
open scoped nonZeroDivisors
universe u v
noncomputable section
namespace GenH2Sol
section Based
variable {L : Type*} [Field L] {F : Type*} [CommRing F] [Algebra L F] {N : ℕ}
  (bF : Module.Basis (Fin (N + 1)) L F)
  (γL : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → L)
  (hγL : ∀ i j m, bF.repr (bF i * bF j) m = γL i j m)
variable (ψL : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → L)

Lean source · statement

theorem ΨL_apply (hψLc : ∀ i j k, ψL i j k = ψL j i k) (x y : F) :
    ΨL bF ψL hψLc x y = Ψf bF ψL x y

theorem

ΨL_one

L234 ↗

AlgebraicCurves.Geometry.Proofs.Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero.GenH2Sol.ΨL_one

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero
open Polynomial
open scoped nonZeroDivisors
universe u v
noncomputable section
namespace GenH2Sol
section Based
variable {L : Type*} [Field L] {F : Type*} [CommRing F] [Algebra L F] {N : ℕ}
  (bF : Module.Basis (Fin (N + 1)) L F)
  (γL : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → L)
  (hγL : ∀ i j m, bF.repr (bF i * bF j) m = γL i j m)
variable (ψL : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → L)

Lean source · statement

theorem ΨL_one (hψLc : ∀ i j k, ψL i j k = ψL j i k) (hone : bF 0 = 1)
    (hψL1 : ∀ j k, ψL 0 j k = 0) (y : F) : ΨL bF ψL hψLc 1 y = 0

theorem

ΨL_coc

L242 ↗

AlgebraicCurves.Geometry.Proofs.Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero.GenH2Sol.ΨL_coc

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero
open Polynomial
open scoped nonZeroDivisors
universe u v
noncomputable section
namespace GenH2Sol
section Based
variable {L : Type*} [Field L] {F : Type*} [CommRing F] [Algebra L F] {N : ℕ}
  (bF : Module.Basis (Fin (N + 1)) L F)
  (γL : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → L)
  (hγL : ∀ i j m, bF.repr (bF i * bF j) m = γL i j m)
variable (ψL : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → L)
include hγL in

Lean source · statement

theorem ΨL_coc (hψLc : ∀ i j k, ψL i j k = ψL j i k) (hγLc : ∀ i j k, γL i j k = γL j i k)
    (hD2 : ∀ i j l m, D2 γL ψL i j l m = 0) (x y z : F) :
    x • ΨL bF ψL hψLc y z - ΨL bF ψL hψLc (x * y) z + ΨL bF ψL hψLc x (y * z) -
      z • ΨL bF ψL hψLc x y = 0

theorem

key

L263 ↗

AlgebraicCurves.Geometry.Proofs.Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero.GenH2Sol.key

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero
open Polynomial
open scoped nonZeroDivisors
universe u v
noncomputable section
namespace GenH2Sol
section Based
variable {L : Type*} [Field L] {F : Type*} [CommRing F] [Algebra L F] {N : ℕ}
  (bF : Module.Basis (Fin (N + 1)) L F)
  (γL : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → L)
  (hγL : ∀ i j m, bF.repr (bF i * bF j) m = γL i j m)
variable (ψL : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → L)
include hγL in

Lean source · full declaration

theorem key (hψLc : ∀ i j k, ψL i j k = ψL j i k) (hγLc : ∀ i j k, γL i j k = γL j i k)
    (l : F →ₗ[L] F)
    (hl : ∀ x y, ΨL bF ψL hψLc x y = l (x * y) - x • l y - y • l x) (i j m : Fin (N + 1)) :
    ψL i j m = -D1 γL (fun i m => bF.repr (l (bF i)) m) i j m := by
  have h := congrArg (fun w => bF.repr w m) (hl (bF i) (bF j))
  have lhs : bF.repr (ΨL bF ψL hψLc (bF i) (bF j)) m = ψL i j m := by
    rw [ΨL_apply, Ψf_repr, repr_basis_eq_single, repr_basis_eq_single, cst_single_single]
  have hbb : bF i * bF j = ∑ k, γL i j k • bF k := by
    conv_lhs => rw [← bF.sum_repr (bF i * bF j)]
    exact Finset.sum_congr rfl fun k _ => by rw [hγL]
  have t1 : bF.repr (l (bF i * bF j)) m = ∑ k, γL i j k * bF.repr (l (bF k)) m := by
    rw [hbb, map_sum, map_sum, Finsupp.finsetSum_apply]
    refine Finset.sum_congr rfl fun k _ => ?_
    rw [map_smul, map_smul, Finsupp.smul_apply, smul_eq_mul]
  have t2 : bF.repr (bF i • l (bF j)) m = ∑ q, bF.repr (l (bF j)) q * γL i q m := by
    rw [smul_eq_mul, repr_mul bF γL hγL, repr_basis_eq_single, cst_single_left]
  have t3 : bF.repr (bF j • l (bF i)) m = ∑ q, bF.repr (l (bF i)) q * γL q j m := by
    rw [smul_eq_mul, repr_mul bF γL hγL, repr_basis_eq_single, cst_single_left]
    exact Finset.sum_congr rfl fun q _ => by rw [hγLc]
  simp only [map_sub, Finsupp.sub_apply] at h
  rw [lhs, t1, t2, t3] at h
  rw [h, D1]
  ring

theorem

main

L297 ↗

AlgebraicCurves.Geometry.Proofs.Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero.GenH2Sol.main

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero
open Polynomial
open scoped nonZeroDivisors
universe u v
noncomputable section
namespace GenH2Sol
section Main
attribute [local instance] FractionRing.liftAlgebra FractionRing.isScalarTower_liftAlgebra
variable {K : Type u} [Field K] {n : ℕ} {B : Type v} [CommRing B] [IsDomain B] [IsIntegrallyClosed
  B]
  [Algebra K[X] B]

Lean source · full declaration

theorem main (b : Module.Basis (Fin (n + 1)) K[X] B) (hb0 : b 0 = 1)
    (hdisc : Algebra.discr K[X] b ≠ 0)
    (ψ : Fin (n + 1) → Fin (n + 1) → Fin (n + 1) → K[X])
    (hψ1 : ∀ j k, ψ 0 j k = 0) (hψc : ∀ i j k, ψ i j k = ψ j i k)
    (hψa : ∀ i j l m, D2 (fun i j k => b.repr (b i * b j) k) ψ 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 (fun i j k => b.repr (b i * b j) k) lam i j m := by
  classical
  let L := FractionRing K[X]
  let F := FractionRing B
  let _ : Module.Finite K[X] B := Module.Finite.of_basis b
  let _ : Module.Free K[X] B := Module.Free.of_basis b
  have hinjB : Function.Injective (algebraMap K[X] B) := by
    intro f g hfg
    have h1 : ∀ f : K[X], b.repr (algebraMap K[X] B f) 0 = f := fun f => by
      rw [Algebra.algebraMap_eq_smul_one, ← hb0, map_smul, b.repr_self, Finsupp.smul_apply,
        Finsupp.single_eq_same, smul_eq_mul, mul_one]
    rw [← h1 f, ← h1 g, hfg]
  let _ : FaithfulSMul K[X] B := (faithfulSMul_iff_algebraMap_injective K[X] B).2 hinjB
  let _ : Algebra.IsIntegral K[X] B := inferInstance
  let _ : IsIntegralClosure B K[X] F := IsIntegralClosure.of_isIntegrallyClosed B K[X] F
  let _ : Algebra.IsAlgebraic L F := isAlgebraic_of_isFractionRing (R := K[X]) (S := B) L F
  let _ : IsLocalization (Algebra.algebraMapSubmonoid B K[X]⁰) F :=
    IsIntegralClosure.isLocalization K[X] L F B
  let bF : Module.Basis (Fin (n + 1)) L F := b.localizationLocalization L K[X]⁰ F
  have hbF : ∀ i, bF i = algebraMap B F (b i) := fun i =>
    Module.Basis.localizationLocalization_apply L K[X]⁰ F b i
  have hbFrepr : ∀ (x : B) (i : Fin (n + 1)), bF.repr (algebraMap B F x) i =
      algebraMap K[X] L (b.repr x i) := fun x i =>
    Module.Basis.localizationLocalization_repr_algebraMap L K[X]⁰ F b x i
  let _ : FiniteDimensional L F := Module.Finite.of_basis bF
  have hdiscL : Algebra.discr L bF ≠ 0 := by
    rw [Algebra.discr_localizationLocalization K[X] K[X]⁰ F b]
    exact fun h => hdisc ((IsFractionRing.injective K[X] L) (by rw [h, map_zero]))
  have hnondeg : (Algebra.traceForm L F).Nondegenerate := by
    apply LinearMap.BilinForm.nondegenerate_of_det_ne_zero (Algebra.traceForm L F) bF
    rw [← Algebra.traceMatrix_of_basis, ← Algebra.discr_def]
    exact hdiscL
  let _ : Algebra.IsSeparable L F := ((traceForm_nondegenerate_tfae L F).out 1 3).2 hnondeg
  let _ : Algebra.FormallyEtale L F := Algebra.FormallyEtale.of_isSeparable L F
  let γL : Fin (n + 1) → Fin (n + 1) → Fin (n + 1) → L := fun i j k =>
    algebraMap K[X] L (b.repr (b i * b j) k)
  let ψL : Fin (n + 1) → Fin (n + 1) → Fin (n + 1) → L := fun i j k => algebraMap K[X] L (ψ i j k)
  have hγL : ∀ i j m, bF.repr (bF i * bF j) m = γL i j m := fun i j m => by
    rw [hbF, hbF, ← map_mul, hbFrepr]
  have hγLc : ∀ i j k, γL i j k = γL j i k := fun i j k => by
    change algebraMap K[X] L (b.repr (b i * b j) k) = algebraMap K[X] L (b.repr (b j * b i) k)
    rw [mul_comm]
  have hψLc : ∀ i j k, ψL i j k = ψL j i k := fun i j k => by
    change algebraMap K[X] L (ψ i j k) = algebraMap K[X] L (ψ j i k)
    rw [hψc]
  have hψL1 : ∀ j k, ψL 0 j k = 0 := fun j k => by
    change algebraMap K[X] L (ψ 0 j k) = 0
    rw [hψ1, map_zero]
  have hD2L : ∀ i j l m, D2 γL ψL i j l m = 0 := fun i j l m => by
    have := congrArg (algebraMap K[X] L) (hψa i j l m)
    rw [D2_map, map_zero] at this
    exact this
  have hbF0 : bF 0 = 1 := by rw [hbF, hb0, map_one]
  obtain ⟨l, hl1, hl⟩ :=
    Algebra.FormallySmooth.exists_linearMap_eq_of_symmetric_hochschild_two_cocycle L F F
      (ΨL bF ψL hψLc) (fun x y => by rw [ΨL_apply, ΨL_apply, Ψf_symm bF ψL hψLc])
      (ΨL_one bF ψL hψLc hbF0 hψL1) (ΨL_coc bF γL hγL ψL hψLc hγLc hD2L)
  have hkey := key bF γL hγL ψL hψLc hγLc l hl
  set lamL : Fin (n + 1) → Fin (n + 1) → L := fun i m => bF.repr (l (bF i)) m with hlamLdef
  have hlamL0 : ∀ m, lamL 0 m = 0 := fun m => by
    change bF.repr (l (bF 0)) m = 0
    rw [hbF0, hl1, map_zero, Finsupp.zero_apply]
  obtain ⟨u, hu⟩ := IsLocalization.exist_integer_multiples_of_finite K[X]⁰
    (fun p : Fin (n + 1) × Fin (n + 1) => -lamL p.1 p.2)
  choose lamf hlamf using fun p : Fin (n + 1) × Fin (n + 1) => hu p
  let lam : Fin (n + 1) → Fin (n + 1) → K[X] := fun i m => lamf (i, m)
  have hlam : ∀ i m, algebraMap K[X] L (lam i m) = (u : K[X]) • (-lamL i m) := fun i m =>
    hlamf (i, m)
  have hu0 : (u : K[X]) ≠ 0 := nonZeroDivisors.coe_ne_zero u
  refine ⟨u, hu0, lam, fun m => ?_, fun i j m => ?_⟩
  · apply IsFractionRing.injective K[X] L
    rw [hlam, hlamL0, neg_zero, smul_zero, map_zero]
  · apply IsFractionRing.injective K[X] L
    rw [map_mul, D1_map]
    have hlam' : (fun i m => algebraMap K[X] L (lam i m)) = ((algebraMap K[X] L u) • (-lamL)) := by
      funext i m
      rw [hlam, Pi.smul_apply, Pi.smul_apply, Pi.neg_apply, Pi.neg_apply, Algebra.smul_def,
        smul_eq_mul]
    rw [hlam', D1_smul, D1_neg]
    change algebraMap K[X] L u * ψL i j m = _
    rw [hkey i j m]

theorem

exists_mul_eq_hochschild_coboundary_of_discr_ne_zero

L391 ↗

AlgebraicCurve.exists_mul_eq_hochschild_coboundary_of_discr_ne_zero

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_mul_eq_hochschild_coboundary_of_discr_ne_zero
open Polynomial
open scoped nonZeroDivisors
universe u v

Lean source · statement

theorem _root_.AlgebraicCurve.exists_mul_eq_hochschild_coboundary_of_discr_ne_zero
    (K : Type u) [Field K] (n : ℕ) (B : Type v) [CommRing B] [IsDomain B] [IsIntegrallyClosed B]
    [Algebra K[X] B] (b : Module.Basis (Fin (n + 1)) K[X] B) (hb0 : b 0 = 1)
    (hdisc : Algebra.discr K[X] b ≠ 0)
    (ψ : Fin (n + 1) → Fin (n + 1) → Fin (n + 1) → K[X])
    (hψ1 : ∀ j k, ψ 0 j k = 0) (hψc : ∀ i j k, ψ i j k = ψ j i k)
    (hψa : ∀ i j l m, (∑ k, ψ j l k * b.repr (b i * b k) m) - (∑ k, b.repr (b i * b j) k * ψ k l m)
      +
        (∑ k, b.repr (b j * b l) k * ψ i k m) - (∑ k, ψ i j k * b.repr (b k * b 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 * b.repr (b i * b k) m) -
        (∑ k, b.repr (b i * b j) k * lam k m) + (∑ k, lam i k * b.repr (b k * b j) m)

Module documentation

Exists mul eq hochschild coboundary of discr ne zero

Declarations