matita/matita/contribs/mf/pisigma.ma

   1 (* (C) 2014 Luca Bressan *)
   2
   3 include "model.ma".
   4
   5 definition epi: ∀B: est. edst B → est ≝
   6  λB,C. mk_est
   7  (Σh: ∀y: sup B. sup (dsup … C y). ∀y1,y2: sup B. ∀d: y1 ≃ y2. subst … d (h y1) ≃ h y2)
   8  (λz,z'. ∀y: sup B. eq … ((sig1 … z) y) ((sig1 … z') y))
   9  ?.
  10  % [ #x #y @(ı…)
  11    | #x #x' #h #y @((h …)⁻¹)
  12    | #x #x' #x'' #h1 #h2 #y @((h1 …)•(h2 …))
  13    ]
  14 qed.
  15
  16 interpretation "Properness of set morphisms" 'ap f d = (sig2 ?? f ?? d).
  17 interpretation "Support of set morphisms" 'sup_f f d = (sig1 ?? f d).
  18
  19 definition eto: est → est → est ≝
  20  λB,C. epi B (constant_edst B C).
  21
  22 definition lift: ∀A,B: est. sup (eto A B) → edst B → edst A ≝
  23  λA,B,f,C.
  24  mk_edst A (λa: sup A. dsup … C (sig1 … f a))
  25  (λx1,x2,d. subst … (sig2 … f … d)) ?.
  26  letin B' ≝ (constant_edst A B)
  27  % [ #x1 #x2 #d #y #y' #e @(pres_eq … e)
  28    | #x1 #x2 #d1 #d2 #y @not_dep
  29    | #x #y
  30      cut (y∘(ı(f˙x)) ≃ y)
  31      [ @pres_id
  32      | cut (y∘(f◽(ıx)) ≃ y∘ı(f˙x))
  33        [ @not_dep
  34        | @tra
  35        ]
  36      ]
  37    | #x1 #x2 #x3 #y #d1 #d2
  38      cut (y∘(f◽d1)∘(f◽d2) ≃ y∘(f◽d1)•(f◽d2))
  39      [ @clos_comp
  40      | cut (y∘(f◽d1)•(f◽d2) ≃ y∘(f◽(d1•d2)))
  41        [ @not_dep
  42        | #e1 #e2 @(e2•e1)
  43        ]
  44      ]
  45    ]
  46 qed.
  47
  48 definition shift: ∀B: est. edst B → est → edst B.
  49  #B #C #D %
  50  [ #b @(eto (C b) D)
  51  | #x1 #x2 #d #f %
  52    [ #y @(f˙(y∘d⁻¹))
  53    | #y1 #y2 #e @(f◽…) @pres_eq @e
  54    ]
  55  | %
  56    [ #x1 #x2 #d #f1 #f2 #h #y @(h (y∘d⁻¹))
  57    | #x1 #x2 #d1 #d2 #f #y @(f◽…) @not_dep
  58    | #x #f #y @(f◽…) cut (y∘(ıx) ≃ y)
  59      [ @pres_id
  60      | #h @tra [ @(y∘(ıx)) | @not_dep | @pres_id ]
  61      ]
  62    | #x1 #x2 #x3 #f #d1 #d2 #y @(f◽…)
  63      @tra [ @(y∘(d2⁻¹•d1⁻¹)) | @clos_comp | @not_dep ]
  64    ]
  65  ]
  66 qed.
  67
  68 definition esigma: ∀B: est. edst B → est ≝
  69  λB,C. mk_est
  70  (Σy: B. C y)
  71  (λz,z'. ∃d: π1 z ≃ π1 z'. (π2 z)∘d ≃ π2 z')
  72  ?.
  73  % [ * #b #c %{ıb} @pres_id
  74    | * #b #c * #b' #c' * #d #h %{(d⁻¹)}
  75      @tra [ @(c∘d•d⁻¹)
  76           | @tra [ @(c∘d∘d⁻¹) | @pres_eq @(h⁻¹) | @clos_comp ]
  77           | @tra [ @(c∘ıb) | @not_dep | @pres_id ]
  78           ]
  79    | * #b #c * #b' #c' * #b'' #c'' * #d1 #h1 * #d2 #h2 %{(d1•d2)}
  80      @tra [ @(c∘d1∘d2)
  81           | @sym @clos_comp
  82           | @tra [ @(c'∘d2) | @pres_eq @h1 | @h2 ]
  83           ]
  84    ]
  85 qed.
  86
  87 definition etimes: est → est → est ≝
  88  λB,C. esigma B (constant_edst B C).
  89
  90 definition mk_esigma: ∀B: est. ∀C: edst B. epi B (shift B C (esigma B C)).
  91  #B #C %
  92  [ #b %
  93    [ #c @〈b, c〉
  94    | #c1 #c2 #d %{(ıb)}
  95      @tra [ @c1 | @pres_id | @d ]
  96    ]
  97  | #b1 #b2 #d #y %{d} @inverse_subst
  98  ]
  99 qed.
 100
 101 definition esig1: ∀B: est. ∀C: edst B. sup (eto (esigma B C) B) ≝
 102  λB,C. 〈π1 …, ?〉.
 103  * #b1 #c1 * #b2 #c2 * #db #dc @db
 104 qed.
 105
 106 definition esig2: ∀B: est. ∀C: edst B. sup (epi (esigma B C) (lift … (esig1 …) C …)) ≝
 107  λB,C. 〈π2 …, ?〉.
 108  * #b1 #c1 * #b2 #c2 * #db #dc @dc
 109 qed.
 110