gaxiiiiiiiiiiii’s gists

gaxiiiiiiiiiiii / Heyting.lean

Created December 12, 2025 22:06

	import Mathlib

	lemma le_iff_inf_compl_eq_bot [BooleanAlgebra B] (x y : B) :
	x ≤ y ↔ x ⊓ yᶜ = ⊥
	:= by
	constructor<;> intro H
	· rw [<- sup_eq_right] at H
	rw [<- H, compl_sup, <- inf_assoc, inf_compl_eq_bot, bot_inf_eq]
	· rw [<- bot_sup_eq (a := y), <- H, sup_inf_right, compl_sup_eq_top, inf_top_eq]
	apply le_sup_left

gaxiiiiiiiiiiii / Krull.lean

Created December 8, 2025 22:31

	import Mathlib

	open Order

	instance Ideal.isCoatomic (B : Type _) [BooleanAlgebra B] :
	IsCoatomic (Ideal B)
	:= {
	eq_top_or_exists_le_coatom I := by
	rw [or_iff_not_imp_left]; intro HI
	let 𝓙 := {J : Ideal B \| J.IsProper ∧ I ≤ J}

gaxiiiiiiiiiiii / EvenLength.lean

Created December 6, 2025 10:58

	variable {α : Type}

	/-- リストの長さが偶数であることを表す述語 -/
	@[grind]
	inductive EvenLength : List α → Prop
	\| nil : EvenLength []
	\| cons_cons {a b : α} {l : List α} (h : EvenLength l) :
	EvenLength (a :: b :: l)

	example (xs : List α) : EvenLength xs ↔ xs.length % 2 = 0 := by

gaxiiiiiiiiiiii / BoolAlg_BoolRing.lean

Created November 16, 2025 12:06

	import Mathlib

	namespace TAL

	class BoolAlg (P : Type) extends DistribLattice P, HasCompl P, BoundedOrder P where
	inf_compl_eq_bot (x : P) : x ⊓ xᶜ = ⊥
	sup_compl_eq_top (x : P) : x ⊔ xᶜ = ⊤

	class BoolRing (P : Type _ )extends Ring P where
	idempotent (a : P) : a * a = a

gaxiiiiiiiiiiii / Epi.lean

Created September 21, 2025 14:11

	-- Notes on regular, exact and additive categories
	-- Marino Gran


	import Mathlib

	open CategoryTheory
	open Limits

	#check Balanced

gaxiiiiiiiiiiii / HasExp.lean

Last active September 11, 2025 09:02

	import Mathlib
	import Mathlib.CategoryTheory.Limits.Shapes.Terminal
	import Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
	import Mathlib.CategoryTheory.Limits.Shapes.Products





	open CategoryTheory

gaxiiiiiiiiiiii / Adj_Represendtable.lean

Created August 29, 2025 14:13

U : 𝓐 ⥤ 𝓑 が右随伴である事、任意のBについてHom(B, U -)が表現可能である事、の同値性を証明

	import Mathlib

	open CategoryTheory

	example [Category 𝓐] [Category 𝓑] (U : 𝓐 ⥤ 𝓑) :
	U.IsRightAdjoint ↔ ∀ B : 𝓑, (U ⋙ coyoneda.obj (Opposite.op B)).IsCorepresentable
	:= by
	constructor<;> intro H
	· rcases H with ⟨F, ⟨σ⟩⟩
	intro B; constructor

gaxiiiiiiiiiiii / RepresentablePreserves.lean

Created August 19, 2025 12:53

	import Mathlib
	import Mathlib.CategoryTheory.Limits.Preserves.Basic


	open CategoryTheory
	open Limits


	example [Category 𝓒] (F : 𝓒ᵒᵖ ⥤ Type v) (HF : F.IsRepresentable) :
	PreservesLimits F

gaxiiiiiiiiiiii / Limit.lean

Created August 7, 2025 06:44

	import Mathlib
	import Mathlib.CategoryTheory.Category.Basic
	import Mathlib.CategoryTheory.Yoneda

	open CategoryTheory
	open Limits


	#check Functor.cones
	/-

gaxiiiiiiiiiiii / PullbackPasting.lean

Created August 4, 2025 10:07

	import Mathlib
	import Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
	import Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone

	open CategoryTheory
	open Limits

	section PB2

	variable [Category 𝓒] (A B C D E F : 𝓒)