quasi-borel-spaces/QuasiBorelSpaces/Quotient.lean at main · YellPika/quasi-borel-spaces · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
module

import QuasiBorelSpaces.Hom
public import QuasiBorelSpaces.Prod
public import QuasiBorelSpaces.Defs

public section

namespace QuasiBorelSpace.Quotient

variable
  {A : Type*} {_ : QuasiBorelSpace A}
  {B : Type*} {_ : QuasiBorelSpace B}
  {C : Type*} {_ : QuasiBorelSpace C}
  {S : Setoid A} {S' : Setoid B}

@[simps]
instance [QuasiBorelSpace A] : QuasiBorelSpace (Quotient S) where
  IsVar φ := ∃ ψ : ℝ → A, IsHom ψ ∧ ∀r, φ r = ⟦ψ r⟧
  isVar_const x := by
    induction x using Quotient.inductionOn with | h x =>
    use fun _ ↦ x
    simp only [isHom_const', implies_true, and_self]
  isVar_comp {f} {φ} hf hφ := by
    rcases hφ with ⟨ψ, hψ, hφ⟩
    use fun x ↦ ψ (f x)
    apply And.intro
    · fun_prop
    · simp only [hφ, implies_true]
  isVar_cases' {index} {φ} hindex hφ := by
    choose ψ hψ hφ using hφ
    use fun r ↦ ψ (index r) r
    apply And.intro
    · apply isHom_cases (by simp only [isHom_ofMeasurableSpace, hindex]) hψ
    · simp only [hφ, implies_true]

@[simp]
lemma isHom_def (φ : ℝ → Quotient S) : IsHom φ ↔ ∃ ψ : ℝ → A, IsHom ψ ∧ ∀r, φ r = ⟦ψ r⟧ := by
  rw [← isVar_iff_isHom]
  rfl

@[simp, fun_prop]
lemma isHom_mk : IsHom (fun x ↦ (⟦x⟧ : Quotient S)) := by
  rw [QuasiBorelSpace.isHom_def]
  simp only [isHom_def, Quotient.eq]
  intro φ hφ
  use φ
  simp only [hφ, true_and]
  intro r
  rfl

@[simp, local fun_prop]
lemma isHom_lift
    {f : A → B} (hf₁ : IsHom f) (hf₂ : ∀ x y, x ≈ y → f x = f y)
    : IsHom (Quotient.lift f hf₂ : Quotient S → B) := by
  rw [QuasiBorelSpace.isHom_def]
  simp only [isHom_def, forall_exists_index, and_imp]
  intro φ ψ hψ hφ
  simp only [hφ, Quotient.lift_mk]
  fun_prop

@[simp, fun_prop]
lemma isHom_lift'
    {f : C → A → B} (hf₁ : IsHom fun (x, y) ↦ f x y) (hf₂ : ∀ x y z, y ≈ z → f x y = f x z)
    {g : C → Quotient S} (hg : IsHom g)
    : IsHom (fun x ↦ Quotient.lift (f x) (hf₂ x) (g x)) := by
  have {x}
      : Quotient.lift (f x) (hf₂ x) (g x)
      = Quotient.lift (β := C →𝒒 B)
          (fun y ↦ .mk (f · y))
          (by intro a b hab
              ext c
              apply hf₂
              exact hab)
          (g x) x := by
    rcases g x with ⟨gx⟩
    simp only [QuasiBorelHom.coe_mk]
  simp only [this]
  fun_prop

end QuasiBorelSpace.Quotient