This repository was archived by the owner on Jul 24, 2024. It is now read-only.
-
Notifications
You must be signed in to change notification settings - Fork 289
Expand file tree
/
Copy pathbasic.lean
More file actions
139 lines (104 loc) · 4.87 KB
/
Copy pathbasic.lean
File metadata and controls
139 lines (104 loc) · 4.87 KB
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
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
/-
Copyright (c) 2021 Scott Morrison. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Scott Morrison
-/
import logic.equiv.set
/-!
# Small types
> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
> Any changes to this file require a corresponding PR to mathlib4.
A type is `w`-small if there exists an equivalence to some `S : Type w`.
We provide a noncomputable model `shrink α : Type w`, and `equiv_shrink α : α ≃ shrink α`.
A subsingleton type is `w`-small for any `w`.
If `α ≃ β`, then `small.{w} α ↔ small.{w} β`.
-/
universes u w v
/--
A type is `small.{w}` if there exists an equivalence to some `S : Type w`.
-/
class small (α : Type v) : Prop :=
(equiv_small : ∃ (S : Type w), nonempty (α ≃ S))
/--
Constructor for `small α` from an explicit witness type and equivalence.
-/
lemma small.mk' {α : Type v} {S : Type w} (e : α ≃ S) : small.{w} α :=
⟨⟨S, ⟨e⟩⟩⟩
/--
An arbitrarily chosen model in `Type w` for a `w`-small type.
-/
@[nolint has_nonempty_instance]
def shrink (α : Type v) [small.{w} α] : Type w :=
classical.some (@small.equiv_small α _)
/--
The noncomputable equivalence between a `w`-small type and a model.
-/
noncomputable
def equiv_shrink (α : Type v) [small.{w} α] : α ≃ shrink α :=
nonempty.some (classical.some_spec (@small.equiv_small α _))
@[priority 100]
instance small_self (α : Type v) : small.{v} α :=
small.mk' $ equiv.refl α
theorem small_map {α : Type*} {β : Type*} [hβ : small.{w} β] (e : α ≃ β) : small.{w} α :=
let ⟨γ, ⟨f⟩⟩ := hβ.equiv_small in small.mk' (e.trans f)
theorem small_lift (α : Type u) [hα : small.{v} α] : small.{max v w} α :=
let ⟨⟨γ, ⟨f⟩⟩⟩ := hα in small.mk' $ f.trans equiv.ulift.symm
@[priority 100]
instance small_max (α : Type v) : small.{max w v} α :=
small_lift.{v w} α
instance small_ulift (α : Type u) [small.{v} α] : small.{v} (ulift.{w} α) :=
small_map equiv.ulift
theorem small_type : small.{max (u+1) v} (Type u) := small_max.{max (u+1) v} _
section
open_locale classical
theorem small_congr {α : Type*} {β : Type*} (e : α ≃ β) : small.{w} α ↔ small.{w} β :=
⟨λ h, @small_map _ _ h e.symm, λ h, @small_map _ _ h e⟩
instance small_subtype (α : Type v) [small.{w} α] (P : α → Prop) : small.{w} { x // P x } :=
small_map (equiv_shrink α).subtype_equiv_of_subtype'
theorem small_of_injective {α : Type v} {β : Type w} [small.{u} β] {f : α → β}
(hf : function.injective f) : small.{u} α :=
small_map (equiv.of_injective f hf)
theorem small_of_surjective {α : Type v} {β : Type w} [small.{u} α] {f : α → β}
(hf : function.surjective f) : small.{u} β :=
small_of_injective (function.injective_surj_inv hf)
theorem small_subset {α : Type v} {s t : set α} (hts : t ⊆ s) [small.{u} s] : small.{u} t :=
let f : t → s := λ x, ⟨x, hts x.prop⟩ in
@small_of_injective _ _ _ f (λ x y hxy, subtype.ext (subtype.mk.inj hxy))
@[priority 100]
instance small_subsingleton (α : Type v) [subsingleton α] : small.{w} α :=
begin
rcases is_empty_or_nonempty α; resetI,
{ apply small_map (equiv.equiv_pempty α) },
{ apply small_map equiv.punit_of_nonempty_of_subsingleton, assumption' },
end
/-!
We don't define `small_of_fintype` or `small_of_countable` in this file,
to keep imports to `logic` to a minimum.
-/
instance small_Pi {α} (β : α → Type*) [small.{w} α] [∀ a, small.{w} (β a)] :
small.{w} (Π a, β a) :=
⟨⟨Π a' : shrink α, shrink (β ((equiv_shrink α).symm a')),
⟨equiv.Pi_congr (equiv_shrink α) (λ a, by simpa using equiv_shrink (β a))⟩⟩⟩
instance small_sigma {α} (β : α → Type*) [small.{w} α] [∀ a, small.{w} (β a)] :
small.{w} (Σ a, β a) :=
⟨⟨Σ a' : shrink α, shrink (β ((equiv_shrink α).symm a')),
⟨equiv.sigma_congr (equiv_shrink α) (λ a, by simpa using equiv_shrink (β a))⟩⟩⟩
instance small_prod {α β} [small.{w} α] [small.{w} β] : small.{w} (α × β) :=
⟨⟨shrink α × shrink β,
⟨equiv.prod_congr (equiv_shrink α) (equiv_shrink β)⟩⟩⟩
instance small_sum {α β} [small.{w} α] [small.{w} β] : small.{w} (α ⊕ β) :=
⟨⟨shrink α ⊕ shrink β,
⟨equiv.sum_congr (equiv_shrink α) (equiv_shrink β)⟩⟩⟩
instance small_set {α} [small.{w} α] : small.{w} (set α) :=
⟨⟨set (shrink α), ⟨equiv.set.congr (equiv_shrink α)⟩⟩⟩
instance small_range {α : Type v} {β : Type w} (f : α → β) [small.{u} α] :
small.{u} (set.range f) :=
small_of_surjective set.surjective_onto_range
instance small_image {α : Type v} {β : Type w} (f : α → β) (S : set α) [small.{u} S] :
small.{u} (f '' S) :=
small_of_surjective set.surjective_onto_image
theorem not_small_type : ¬ small.{u} (Type (max u v))
| ⟨⟨S, ⟨e⟩⟩⟩ := @function.cantor_injective (Σ α, e.symm α)
(λ a, ⟨_, cast (e.3 _).symm a⟩)
(λ a b e, (cast_inj _).1 $ eq_of_heq (sigma.mk.inj e).2)
end