Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Injective, surjective and isomorphic terms

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

definition

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Definition

    Definition 5.4. A rational term f:A→Bf : A \to B is

    • injective if f;f−1≡idf \mathbin{;} f^{-1} \equiv \mathrm{id} for some term f−1:B→Af^{-1} : B \to A;
    • surjective if f−1;f≡idf^{-1} \mathbin{;} f \equiv \mathrm{id} for some term f−1:B→Af^{-1} : B \to A;
    • an isomorphism if both hold for the same term f−1f^{-1}.

    In categorical terms, an injective term is a section and a surjective term is a retraction in the category of rational terms modulo ≡\equiv.

    Concept map
    5 concepts; 4 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Lax149335.EquationalTheory
    2
    3/-!
    4---
    5title: Injective, surjective and isomorphic terms
    6type: definition
    7---
    8**Definition 5.4.** A rational term f:A→Bf : A \to B is
    9
    10- *injective* if f;f−1≡idf \mathbin{;} f^{-1} \equiv \mathrm{id} for some term f−1:B→Af^{-1} : B \to A;
    11- *surjective* if f−1;f≡idf^{-1} \mathbin{;} f \equiv \mathrm{id} for some term
    12 f−1:B→Af^{-1} : B \to A;
    13- an *isomorphism* if both hold for the same term f−1f^{-1}.
    14
    15In categorical terms, an injective term is a section and a surjective term is a retraction
    16in the category of rational terms modulo ≡\equiv.
    17
    18# Formalization notes
    19
    20The notions are called `ProvablyInjective`, `ProvablySurjective` and `ProvableIso`, to
    21distinguish them from injectivity and surjectivity of the denotation.
    22-/
    23
    24namespace Lax149335.InjectiveSurjectiveTerms
    25
    26open Lax149335.Types Lax149335.Terms Lax149335.EquationalTheory
    27
    28/-- `f : A → B` is injective if `f ; f' ≡ id` for some `f' : B → A`. -/
    29def ProvablyInjective {A B : Ty} (f : Term A B) : Prop :=
    30 ∃ f' : Term B A, (f ⨟ f') ≡ₜ Term.id A
    31
    32/-- `f : A → B` is surjective if `f' ; f ≡ id` for some `f' : B → A`. -/
    33def ProvablySurjective {A B : Ty} (f : Term A B) : Prop :=
    34 ∃ f' : Term B A, (f' ⨟ f) ≡ₜ Term.id B
    35
    36/-- `f : A → B` is an isomorphism if `f ; f' ≡ id` and `f' ; f ≡ id` for some
    37`f' : B → A`. -/
    38def ProvableIso {A B : Ty} (f : Term A B) : Prop :=
    39 ∃ f' : Term B A, (f ⨟ f') ≡ₜ Term.id A ∧ (f' ⨟ f) ≡ₜ Term.id B
    40
    41end Lax149335.InjectiveSurjectiveTerms
    42
    Formalization notes

    The notions are called ProvablyInjectiveProvablyInjective, ProvablySurjectiveProvablySurjective and ProvableIsoProvableIso, to distinguish them from injectivity and surjectivity of the denotation.

    Builds on
    Used by
    From Mathlib

    none

    Discussion

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

    Loading discussion…