Shamrock-Frost

import category_theory.limits.cones algebra.homology.homological_complex

section

open category_theory category_theory.limits homological_complex

universes u u' v v' idx

def homological_complex.cone_of_degreewise_cones
  {J : Type u} [category.{u'} J] {V : Type v} [category.{v'} V] [has_zero_morphisms V]

Shamrock-Frost

import algebra.category.Module.abelian
import algebra.category.Module.images
import algebra.homology.homology
import algebra.homology.Module
import algebra.homology.homotopy

open category_theory category_theory.limits

section

Shamrock-Frost

import tactic

class has_oplus (α : Type*) := (oplus : α → α → α)
class has_otimes (α : Type*) := (otimes : α → α → α)

instance : has_oplus ℤ := { oplus := int.add }
instance : has_otimes ℤ := { otimes := int.mul }

infixl ` ⊕ `:65  := has_oplus.oplus
infixl ` ⊗ `:70  := has_otimes.otimes

Shamrock-Frost

import topology.subset_properties
import topology.connected
import topology.nhds_set
import topology.inseparable
import topology.separation
import topology.maps

open function set filter topological_space
open_locale topological_space filter classical
                             

Shamrock-Frost

import java.io.*;

public class Main {
	public static void main(String[] args) throws IOException {
		File file = new File("test.txt");
		file.createNewFile();
		A a = new A(file);
		a.sayHello();
		a.solveEquations(0,1,2);
		System.out.close();

Shamrock-Frost

Require Import Arith Lia List String.

Set Implicit Arguments.

Definition eq_dec (A : Type) :=
  forall (x : A),
    forall (y : A),
      {x = y} + {x <> y}.

Notation var := string.

Shamrock-Frost

# sadly sage doesn't let me have symbolic variables taking values in Q(u)
# so we need to look include those variables in the definition
K = FractionField(PolynomialRing(QQ, ['u', 'a', 'b', 'c', 'd', 'e', 'f', 'g', 'h', 'i', 'j']))
u, a, b, c, d, e, f, g, h, i, j = K.gens()
# taking u = sqrt(t) we get the R-matrix for the Jones polynomial
R = matrix(K, 4, [-u, 0, 0, 0,  0, u^3 - u, -u^2, 0,  0, -u^2, 0, 0,  0, 0, 0, -u])
mu = matrix(K, 2, [-u, 0,  0, -1/u])

D = matrix(K, 4, [-u, 0, 0, 0,  0, -u, 0, 0,  0, 0, -u, 0,  0, 0, 0, u^3])
P = matrix(K, 4, [0, 0, 1, 0,  0, 1/u, 0, -u,  0, 1, 0, 1,  1, 0, 0, 0])

Shamrock-Frost

import .power

section order

definition minimal_lt (P : ℕ → Prop) [decidable_pred P]
  : ℕ → option (Σ' k : ℕ, P k)
| 0 := none
| (n+1) := minimal_lt n
        <|> (if h' : P n then some ⟨n, h'⟩ else none)

Shamrock-Frost

#lang racket

(define (dict-order f)
  (λ (xs ys)
    (or (null? xs)
        (and (not (null? ys))
             (or (f (car xs) (car ys))
                 (and (equal? (car xs) (car ys))
                      (not (and (null? (cdr xs))
                                (null? (cdr ys))))

Shamrock-Frost

namespace hall_witt

class group (G : Type) :=
(mul : G → G → G)
(mul_assoc : ∀ (a b c : G), mul (mul a b) c = mul a (mul b c))
(one : G)
(one_mul : ∀ (a : G), mul one a = a)
(mul_one : ∀ (a : G), mul a one = a)
(inv : G → G)
(mul_left_inv : ∀ (a : G), mul (inv a) a = one)