jcommelin’s gists

jcommelin / toplevel-2025-03-13.html

Last active March 13, 2025 04:56

toplevel 2025-03-13

	<?xml version="1.0" encoding="UTF-8" ?>
	<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
	<!-- This file was created with the aha Ansi HTML Adapter. https://github.com/theZiz/aha -->
	<html xmlns="http://www.w3.org/1999/xhtml">
	<head>
	<meta http-equiv="Content-Type" content="application/xml+xhtml; charset=UTF-8"/>
	<title>stdin</title>
	</head>
	<body>
	<pre>

jcommelin / FunctorCategory.lean

Last active August 29, 2024 12:01

	universe u v w v₁ v₂ v₃ u₁ u₂ u₃

	section Mathlib.Algebra.Group.ZeroOne

	class Zero (α : Type u) where
	zero : α

	instance (priority := 300) Zero.toOfNat0 {α} [Zero α] : OfNat α (nat_lit 0) where
	ofNat := ‹Zero α›.1

jcommelin / gist:1299f6a0b10e823c96bb251902f209ef

Last active January 18, 2023 19:42

to_additive #align failures

	❌ le_of_forall_neg_add_le <- ✅ le_of_forall_lt_one_mul_le
	❌ le_iff_forall_neg_add_le <- ✅ le_iff_forall_lt_one_mul_le
	❌ Sum.FaithfulVAddLeft <- ✅ Sum.FaithfulSMulLeft
	❌ nsmul_le_nsmul_iff <- ✅ pow_le_pow_iff'
	❌ Multiset.sum_zero <- ✅ Multiset.prod_zero
	❌ nsmul_lt_nsmul_iff <- ✅ pow_lt_pow_iff'
	❌ Part.left_dom_of_sub_dom <- ✅ Part.left_dom_of_div_dom
	❌ Pi.update_eq_sub_add_single <- ✅ Pi.update_eq_div_mul_mulSingle
	❌ eq_zero_or_pos <- ✅ eq_one_or_one_lt
	❌ WithBot.coe_eq_zero <- ✅ WithBot.coe_eq_one

jcommelin / classes.lean

Created September 7, 2022 07:18

IMPAN demo: classes

	import demo.structures

	/-! # Classes

	Define a class (e.g. `monoid`)
	and define an instance (e.g. product monoid).

	-/

	namespace impan

jcommelin / structures.lean

Created September 7, 2022 07:16

IMPAN demo: structures

	import category_theory.category.basic

	open category_theory

	/-! # Structures

	Define your own structure
	(e.g. `prod` or `functor`)
	and define examples (e.g. composition).

jcommelin / yoneda_done.lean

Created September 6, 2022 17:03

Yoneda embedding is fully faithful

	import category_theory.yoneda
	import tactic.apply_fun

	.

	open category_theory opposite

	/-! # Yoneda -/

jcommelin / yoneda.lean

Last active September 6, 2022 08:18

Yoneda template

	import category_theory.yoneda
	import tactic.apply_fun

	.

	open category_theory opposite

	/-! # Yoneda -/

	variables (C : Type) [category.{0} C]

jcommelin / treeshake.lean

Last active July 20, 2022 07:19

Lean file for treeshaking LTE

	import tactic.find_unused
	import challenge

	open tactic

	meta def file_list : list (option string) :=
	["backup/delta_functor.lean", "backup/extr.lean",
	"backup/extr_backup.lean", "backup/multilinear.lean",
	"backup/prepresentation.lean", "backup/sheafification_mono.lean",
	"scripts/lean_version.lean", "scripts/lint_project.lean",

jcommelin / treeshake.txt

Last active July 20, 2022 07:21

Treeshaking LTE e02550056c896599ed0731b93c0e868124b62e88

	AddCommGroup.Ab.category_theory.limits.has_colimits_of_size
	AddCommGroup.colimit_comparison
	AddCommGroup.direct_sum_bicone
	AddCommGroup.direct_sum_punit_iso
	AddCommGroup.hom_product_comparison
	AddCommGroup.is_bilimit_direct_sum_bicone
	AddCommGroup.is_iso_hom_product_comparison
	AddCommGroup.is_limit_pi_fan
	AddCommGroup.pi_fan
	AddCommGroup.pi_lift

jcommelin / henselian_etale.lean

Created September 4, 2021 09:27

Additions to henselian.lean after good etale API

	/-
	TODO: it's not clear to me (jmc) whether the following items can be easily included,
	maybe they depend on theory of etale algebras, just like the items further below

	∀ (f : polynomial R) (a₀ : R) (h₁ : f.eval a₀ ∈ maximal_ideal R)
	(h₂ : f.derivative.eval a₀ ∉ maximal_ideal R),
	∃ a : R, f.is_root a ∧ (a - a₀ ∈ maximal_ideal R),
	∀ (f : polynomial R) (a₀ : residue_field R) (h₁ : aeval a₀ f = 0)
	(h₂ : aeval a₀ f.derivative ≠ 0),
	∃ a : R, f.is_root a ∧ (residue R a = a₀),

Johan Commelin jcommelin