Shamrock-Frost

import Mathlib

namespace TensorProduct

variable {R P Q M : Type*} [CommRing R] [AddCommGroup P] [AddCommGroup Q]
    [AddCommGroup M] [Module R P] [Module R Q] [Module R M]

open LinearMap

theorem map₂_eq_range_lift_comp_mapIncl (f : P →ₗ[R] Q →ₗ[R] M)

Shamrock-Frost

import Mathlib.CategoryTheory.Adjunction.Basic
import Mathlib.CategoryTheory.Monad.Algebra
import Mathlib.CategoryTheory.Conj
import Mathlib.Tactic.TFAE

namespace CategoryTheory

variable {C : Type*} [Category C] {D : Type*} [Category D] {F : C ⥤ D} {G : D ⥤ C}
  {E : Type*} [Category E] {H : D ⥤ E} {K : E ⥤ D}

Shamrock-Frost

def followablePaths : Tree α → List Path
  | nil => []
  | node _ l r => List.map Path.right (followablePaths r)
                  ++ List.map Path.left (followablePaths l)
                  ++ [Path.here]

lemma followablePaths_order : ∀ (p q : Path) (t : Tree α),
    List.Sublist ({p, q} : List Path) (followablePaths t)
    ↔ (p.validFor t ∧ q.validFor t
      ∧ (q ≤ p ∨ (p ⊓ q ++ Path.left Path.here ≤ q

Shamrock-Frost

import Mathlib.CategoryTheory.Action
import Mathlib.CategoryTheory.Category.Cat
import Mathlib.CategoryTheory.DiscreteCategory
import Mathlib.CategoryTheory.Functor.Category
import Mathlib.CategoryTheory.Functor.Hom
import Mathlib.CategoryTheory.Sigma.Basic
import Mathlib.CategoryTheory.Limits.Shapes.Types

open CategoryTheory CategoryTheory.Limits Equiv

Shamrock-Frost

\begin{center}
    \begin{tikzpicture}
        \coordinate (a) at (-1.6, -0.1);
        \coordinate (b) at (0, -1.0);
        \coordinate (c) at (1.2, 0.4);
        \coordinate (d) at (0, 1.5);
        \draw[->, shorten >=4pt, shorten <=4pt] (a) to node[below left] {$p$} (b);
        \draw[->, shorten >=4pt, shorten <=4pt] (b) to node[below right] {$q$} (c);
        \draw[->, shorten >=4pt, shorten <=4pt] (c) to node[above right] {$r$} (d);
        \draw[dashed, shorten >=4pt, shorten <=4pt] (a) -- (c);

Shamrock-Frost

# parameter
for r in range(100):
    R = IntegerModRing(r^3)

    a = r
    b = r^2

    #koszul complex on (a, b) (shifted by 2)
    d0 = matrix(ZZ, 2, 1, [b, -a])
    d1 = matrix(ZZ, 1, 2, [a, b])

Shamrock-Frost

import Mathlib.Order.CompleteBooleanAlgebra
import Mathlib.Topology.Basic
import Mathlib.Topology.Bases
import Mathlib.Topology.Sets.Opens
import Mathlib.CategoryTheory.Adjunction.Basic
import Mathlib.CategoryTheory.Opposites
import Mathlib.Topology.Category.TopCat.Basic
import Mathlib.Order.Category.FrmCat

open CategoryTheory Topology TopologicalSpace

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

R: Type
X: Top
j: ℕ
_inst_2: comm_ring R
i_fst: (singular_chain_complex_basis R (j + 1)).indices
σ: (singular_chain_complex_basis R (j + 1)).models i_fst ⟶ X
⊢ ⇑(((singular_chain_complex R).obj X).d (j + 1) j)
    (⇑((singular_chain_complex R ⋙ homological_complex.eval (Module R) (complex_shape.down ℕ) (j + 1)).map σ)
       (⇑(cone_construction_hom R
             (barycenter

Shamrock-Frost

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

section

open category_theory category_theory.limits homological_complex opposite