Direct and inverse image for functions

Require Export sets functions.

Section Image.

  Variable A B : Type.

  Definition direct_img(f : AB)(P : set A) : set B :=
    fun(b : B) ⇒ (a : A), f a = b P a.

  Definition inv_img(f : AB)(P : set B) : set A :=
    fun(a : A) ⇒ P (f a).

inverse image

  Lemma set_equal_inv_img :
    (f g : AB)(P Q : set B),
      f gset_equal P Qset_equal (inv_img f P) (inv_img g Q).

  Lemma set_equal_inv_img_pred : (f : AB)(P Q : set B),
    set_equal P Qset_equal (inv_img f P) (inv_img f Q).

  Lemma set_equal_inv_img_feq : (f g : AB)(P : set B),
    f gset_equal (inv_img f P) (inv_img g P).

direct image

  Lemma feq_direct_img :
    (f g : AB)(P Q : set A),
      f gset_equal P Qset_equal (direct_img f P) (direct_img g Q).


  Lemma fibred_set_inverse : (f : AB)(P : set B),
    set_inverse (inv_img f P) = inv_img f (set_inverse P).

  Lemma fibred_intersection : (f : AB)(P Q : set B),
    intersection (inv_img f P) (inv_img f Q) =
      inv_img f (intersection P Q).

End Image.

Implicit Arguments direct_img [A B].
Implicit Arguments inv_img [A B].

Other results

Lemma inv_img_id : {A : Type}(P : set A),
  inv_img id P = P.

Lemma inv_img_compose :
  (A B C : Type)(f : AB)(g : BC)(P : set C),
    inv_img f (inv_img g P) = inv_img (g f) P.

This following lemma is the core of the "elementary boolean algebra" reasoning in Lemma 4.13 on page 23. Actually, what is really needed there is the same result with assumption
       is_full_set (set_inverse (intersection
                                  (set_inverse (inv_img pi_1 P))
                                  (set_inverse (inv_img pi_2 Q))))
However, then this lemma is only valid in classical logic, see classic_axiom_neg_disjunction_other_case in classic.v I leave the classical reasoning to the uses of this lemma.
Lemma inv_proj_full :
  (A B : Type)(pi_1 : A × BA)(pi_2 : A × BB)
        (P : set A)(Q : set B)(b : B),
    pi_1 (@fst A B)
    pi_2 (@snd A B)
    is_full_set (union (inv_img pi_1 P) (inv_img pi_2 Q)) →
    not (Q b) →
      is_full_set (inv_img pi_1 P).

Lemma direct_image_left_adjoint :
  (A B : Type)(f : AB)(P : set A)(Q : set B),
    subset P (inv_img f Q) subset (direct_img f P) Q.