theory.jections

Require Import
  Relation_Definitions Basics
  abstract_algebra canonical_names workaround_tactics.
Require theory.setoids.

LocalLocal
Instance id_injective `{Setoid A} : Injective (@id A).

Section compositions.
  Context `{Equiv A} `{Equiv B} `{Equiv C} (g: A B) (f: B C) `{!Inverse f} `{!Inverse g}.

  Global Instance: Inverse (f g) := g⁻¹ f⁻¹.

  Global Instance: Injective f Injective g Injective (f g).

  Global Instance: Surjective f Surjective g Surjective (f g).

  Global Instance: Bijective f Bijective g Bijective (f g) := {}.

End compositions.

Lemma back `{Bijective A B f}: f ⁻¹ f = id.
Lemma surjective_applied `{Surjective A B f} x : f (f⁻¹ x) = x.

Lemma surjective_applied' `{Equiv A} `{Equiv B} (f : A B) `{!Inverse f} `{!Surjective f} x : f (f⁻¹ x) = x.

Lemma bijective_applied `{Bijective A B f} x: f⁻¹ (f x) = x.

Lemma alt_injective `{Equiv A} `{Equiv B} `{f: A B} `{!Inverse f}:
  Setoid_Morphism f
  Setoid_Morphism (f ⁻¹: B A)
  f ⁻¹ f = id Injective f.

Instance: `{Bijective A B f}, Setoid_Morphism (f⁻¹).

Instance: `{Inverse A B f}, Inverse (f ⁻¹) := λ _ _ f _, f.

Lemma flip_bijection_pseudoinstance: `{Bijective A B f}, Bijective (f ⁻¹).

Hint Extern 4 (Bijective (_ ⁻¹)) => apply flip_bijection_pseudoinstance: typeclass_instances.

Lemma flip_bijection `{Equiv A} `{Equiv B} (f: A B) `{!Inverse f}: Bijective (f ⁻¹) Bijective f.


Lemma cancel_left `{Bijective A B f} x y: f x = y x = f ⁻¹ y.

Lemma cancel_left' `{Bijective A B f} x y: f ⁻¹ x = y x = f y.

Instance Injective_proper `{Equiv A} `{Equiv B}: Proper ((=) ==> (=)) (@Injective A B _ _).

Instance Surjective_proper `{Equiv A} `{Equiv B} (f g: A B) {finv: Inverse f}:
  f = g Surjective g (inv:=finv) Surjective f.