The binary hole relation

Lax342547.HoleRelation · concepts/Lax342547/HoleRelation.lean · lax-342547

definition

Loading review…

Natural Language Statement

Definition

Fix binary vector spaces $X,V$ , a functional $a:X\to\mathbb F_2$ , and a symmetric bilinear form $T$ on $X$ . For each raw vertex $i$ , let $U_i:X\to V$ be injective and $u_i:V\to\mathbb F_2$ linear.

A hole between $i,j$ has witnesses $x,y\in X$ satisfying $U_i x=U_j y$ , $u_jU_i=a+T(x,\cdot)$ , $u_iU_j=a+T(y,\cdot)$ , and $a(x)+a(y)=1$ . These are the equations of Definition 2.1.

Concept map

1 concept

100%

DefinitionThis conceptDescendants are omitted for concepts with more than 10 descendants.

Lean source view on GitHub

Show types on hover

1	import Mathlib.Data.ZMod.Basic
2	import Mathlib.LinearAlgebra.BilinearForm.Basic
3
4	/-!
5	---
6	title: The binary hole relation
7	type: definition
8	---
9	Fix binary vector spaces $X,V$ , a functional $a:X\to\mathbb F_2$ , and a
10	symmetric bilinear form $T$ on $X$ . For each raw vertex $i$ , let
11	$U_i:X\to V$ be injective and $u_i:V\to\mathbb F_2$ linear.
12
13	A hole between $i,j$ has witnesses $x,y\in X$ satisfying
14	$U_i x=U_j y$ , $u_jU_i=a+T(x,\cdot)$ ,
15	$u_iU_j=a+T(y,\cdot)$ , and $a(x)+a(y)=1$ .
16	These are the equations of Definition 2.1.
17	-/
18
19	namespace Lax342547.HoleRelation
20
21	universe u v w
22
23	structure HoleData (Ω : Type u) (X : Type v) (V : Type w)
24	[AddCommGroup X] [Module (ZMod 2) X]
25	[AddCommGroup V] [Module (ZMod 2) V] where
26	a : X →ₗ[ZMod 2] ZMod 2
27	T : LinearMap.BilinForm (ZMod 2) X
28	symmetric : ∀ x y, T x y = T y x
29	U : Ω → X →ₗ[ZMod 2] V
30	injective : ∀ i, Function.Injective (U i)
31	u : Ω → V →ₗ[ZMod 2] ZMod 2
32
33	variable {Ω : Type u} {X : Type v} {V : Type w}
34	variable [AddCommGroup X] [Module (ZMod 2) X]
35	variable [AddCommGroup V] [Module (ZMod 2) V]
36
37	def Hole (D : HoleData Ω X V) (i j : Ω) : Prop :=
38	∃ x y : X, D.U i x = D.U j y ∧
39	(∀ z, D.u j (D.U i z) = D.a z + D.T x z) ∧
40	(∀ z, D.u i (D.U j z) = D.a z + D.T y z) ∧
41	D.a x + D.a y = 1
42
43	end Lax342547.HoleRelation
44

Builds on

none

Used by

From Mathlib

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

Loading discussion…

Lax Lean Archive

The binary hole relation

Flags

Flag this concept

Natural Language Statement

Definition

Lean source view on GitHub

Discussion

Settings

Your comments