Cancelling injective and surjective terms

Lax149335.Cancellation · concepts/Lax149335/Cancellation.lean · lax-149335

proven

Loading review…

Lemma 5.5. For all terms $g_1, g_2 : A \to B$ ,

\begin{aligned} g_1 \equiv g_2 &\quad\text{iff}\quad g_1 \mathbin{;} f \equiv g_2 \mathbin{;} f &&\text{for every injective } f : B \to C, \\ g_1 \equiv g_2 &\quad\text{iff}\quad f \mathbin{;} g_1 \equiv f \mathbin{;} g_2 &&\text{for every surjective } f : C \to A. \end{aligned}

Concept map

6 concepts

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Evidence

Each proof establishes this claim relative to its assumptions.

Show types on hover

1	import Lax149335.InjectiveSurjectiveTerms
2
3	/-!
4	---
5	title: Cancelling injective and surjective terms
6	type: lemma
7	---
8	Lemma 5.5. For all terms $g_1, g_2 : A \to B$ ,
9
10	$\begin{aligned} g_1 \equiv g_2 &\quad\text{iff}\quad g_1 \mathbin{;} f \equiv g_2 \mathbin{;} f &&\text{for every injective } f : B \to C, \\ g_1 \equiv g_2 &\quad\text{iff}\quad f \mathbin{;} g_1 \equiv f \mathbin{;} g_2 &&\text{for every surjective } f : C \to A. \end{aligned}$
11
12
13
14
15
16
17	-/
18
19	namespace Lax149335.Cancellation
20
21	open Lax149335.Types Lax149335.Terms Lax149335.EquationalTheory Lax149335.InjectiveSurjectiveTerms
22
23	/-- Lemma 5.5. Injective terms can be cancelled on the right and surjective terms on
24	the left. -/
25	axiom cancel {A B : Ty} (g₁ g₂ : Term A B) :
26	(∀ (C : Ty) (f : Term B C), ProvablyInjective f → (g₁ ≡ₜ g₂ ↔ (g₁ ⨟ f) ≡ₜ (g₂ ⨟ f))) ∧
27	(∀ (C : Ty) (f : Term C A), ProvablySurjective f → (g₁ ≡ₜ g₂ ↔ (f ⨟ g₁) ≡ₜ (f ⨟ g₂)))
28
29	end Lax149335.Cancellation
30

Builds on

Used by

none

From Mathlib

none

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

Loading discussion…

Lax Lean Archive