refactor(category_theory): custom structure for full_subcategory (#14767

)

Full subcategories are now a custom structure rather than the usual subtype. The advantage of this is that we don't have to fight the `simp`-normal form of subtypes, as the coercion does more harm than good for full subcategories.

We saw a similar refactor for discrete categories, and in both cases, erring on the side of explicitness seems to pay off.

src/algebra/category/FinVect.lean

@@ -32,21 +32,15 @@ instance monoidal_predicate_finite_dimensional :
   prop_tensor' := λ X Y hX hY, by exactI module.finite.tensor_product K X Y }
 
 /-- Define `FinVect` as the subtype of `Module.{u} K` of finite dimensional vector spaces. -/
-@[derive [large_category, λ α, has_coe_to_sort α (Sort*), concrete_category, monoidal_category,
-  symmetric_category]]
-def FinVect := { V : Module.{u} K // finite_dimensional K V }
+@[derive [large_category, concrete_category, monoidal_category, symmetric_category]]
+def FinVect := full_subcategory (λ (V : Module.{u} K), finite_dimensional K V)
 
 namespace FinVect
 
-instance finite_dimensional (V : FinVect K) : finite_dimensional K V := V.prop
+instance finite_dimensional (V : FinVect K) : finite_dimensional K V.obj := V.property
 
 instance : inhabited (FinVect K) := ⟨⟨Module.of K K, finite_dimensional.finite_dimensional_self K⟩⟩
 
-instance : has_coe (FinVect.{u} K) (Module.{u} K) := { coe := λ V, V.1, }
-
-protected lemma coe_comp {U V W : FinVect K} (f : U ⟶ V) (g : V ⟶ W) :
-  ((f ≫ g) : U → W) = (g : V → W) ∘ (f : U → V) := rfl
-
 /-- Lift an unbundled vector space to `FinVect K`. -/
 def of (V : Type u) [add_comm_group V] [module K V] [finite_dimensional K V] : FinVect K :=
 ⟨Module.of K V, by { change finite_dimensional K V, apply_instance }⟩
@@ -61,42 +55,39 @@ variables (V : FinVect K)
 
 /-- The dual module is the dual in the rigid monoidal category `FinVect K`. -/
 def FinVect_dual : FinVect K :=
-⟨Module.of K (module.dual K V), subspace.module.dual.finite_dimensional⟩
-
-instance : has_coe_to_fun (FinVect_dual K V) (λ _, V → K) :=
-{ coe := λ v, by { change V →ₗ[K] K at v, exact v, } }
+⟨Module.of K (module.dual K V.obj), subspace.module.dual.finite_dimensional⟩
 
 open category_theory.monoidal_category
 
 /-- The coevaluation map is defined in `linear_algebra.coevaluation`. -/
 def FinVect_coevaluation : 𝟙_ (FinVect K) ⟶ V ⊗ (FinVect_dual K V) :=
-by apply coevaluation K V
+by apply coevaluation K V.obj
 
 lemma FinVect_coevaluation_apply_one : FinVect_coevaluation K V (1 : K) =
-   ∑ (i : basis.of_vector_space_index K V),
-    (basis.of_vector_space K V) i ⊗ₜ[K] (basis.of_vector_space K V).coord i :=
-by apply coevaluation_apply_one K V
+   ∑ (i : basis.of_vector_space_index K V.obj),
+    (basis.of_vector_space K V.obj) i ⊗ₜ[K] (basis.of_vector_space K V.obj).coord i :=
+by apply coevaluation_apply_one K V.obj
 
 /-- The evaluation morphism is given by the contraction map. -/
 def FinVect_evaluation : (FinVect_dual K V) ⊗ V ⟶ 𝟙_ (FinVect K) :=
-by apply contract_left K V
+by apply contract_left K V.obj
 
 @[simp]
-lemma FinVect_evaluation_apply (f : (FinVect_dual K V)) (x : V) :
-  (FinVect_evaluation K V) (f ⊗ₜ x) = f x :=
+lemma FinVect_evaluation_apply (f : (FinVect_dual K V).obj) (x : V.obj) :
+  (FinVect_evaluation K V) (f ⊗ₜ x) = f.to_fun x :=
 by apply contract_left_apply f x
 
 private theorem coevaluation_evaluation :
   let V' : FinVect K := FinVect_dual K V in
   (𝟙 V' ⊗ (FinVect_coevaluation K V)) ≫ (α_ V' V V').inv ≫ (FinVect_evaluation K V ⊗ 𝟙 V')
   = (ρ_ V').hom ≫ (λ_ V').inv :=
-by apply contract_left_assoc_coevaluation K V
+by apply contract_left_assoc_coevaluation K V.obj
 
 private theorem evaluation_coevaluation :
   (FinVect_coevaluation K V ⊗ 𝟙 V)
   ≫ (α_ V (FinVect_dual K V) V).hom ≫ (𝟙 V ⊗ FinVect_evaluation K V)
   = (λ_ V).hom ≫ (ρ_ V).inv :=
-by apply contract_left_assoc_coevaluation' K V
+by apply contract_left_assoc_coevaluation' K V.obj
 
 instance exact_pairing : exact_pairing V (FinVect_dual K V) :=
 { coevaluation := FinVect_coevaluation K V,
@@ -112,7 +103,7 @@ variables {K V} (W : FinVect K)
 
 /-- Converts and isomorphism in the category `FinVect` to a `linear_equiv` between the underlying
 vector spaces. -/
-def iso_to_linear_equiv {V W : FinVect K} (i : V ≅ W) : V ≃ₗ[K] W :=
+def iso_to_linear_equiv {V W : FinVect K} (i : V ≅ W) : V.obj ≃ₗ[K] W.obj :=
   ((forget₂ (FinVect.{u} K) (Module.{u} K)).map_iso i).to_linear_equiv
 
 lemma iso.conj_eq_conj {V W : FinVect K} (i : V ≅ W) (f : End V) :

src/algebra/category/FinVect/limits.lean

@@ -48,7 +48,7 @@ instance (F : J ⥤ FinVect k) :
   finite_dimensional k (limit (F ⋙ forget₂ (FinVect k) (Module.{v} k)) : Module.{v} k) :=
 begin
   haveI : ∀ j, finite_dimensional k ((F ⋙ forget₂ (FinVect k) (Module.{v} k)).obj j),
-  { intro j, change finite_dimensional k (F.obj j), apply_instance, },
+  { intro j, change finite_dimensional k (F.obj j).obj, apply_instance, },
   exact finite_dimensional.of_injective
     (limit_subobject_product (F ⋙ forget₂ (FinVect k) (Module.{v} k)))
     ((Module.mono_iff_injective _).1 (by apply_instance)),

src/algebraic_geometry/AffineScheme.lean

@@ -41,7 +41,8 @@ namespace algebraic_geometry
 open Spec (structure_sheaf)
 
 /-- The category of affine schemes -/
-def AffineScheme := Scheme.Spec.ess_image
+@[derive category, nolint has_nonempty_instance]
+def AffineScheme := Scheme.Spec.ess_image_subcategory
 
 /-- A Scheme is affine if the canonical map `X ⟶ Spec Γ(X)` is an isomorphism. -/
 class is_affine (X : Scheme) : Prop :=
@@ -54,18 +55,23 @@ def Scheme.iso_Spec (X : Scheme) [is_affine X] :
   X ≅ Scheme.Spec.obj (op $ Scheme.Γ.obj $ op X) :=
 as_iso (Γ_Spec.adjunction.unit.app X)
 
-lemma mem_AffineScheme (X : Scheme) : X ∈ AffineScheme ↔ is_affine X :=
+/-- Construct an affine scheme from a scheme and the information that it is affine. -/
+@[simps]
+def AffineScheme.mk (X : Scheme) (h : is_affine X) : AffineScheme :=
+⟨X, @@mem_ess_image_of_unit_is_iso _ _ _ _ h.1⟩
+
+lemma mem_Spec_ess_image (X : Scheme) : X ∈ Scheme.Spec.ess_image ↔ is_affine X :=
 ⟨λ h, ⟨functor.ess_image.unit_is_iso h⟩, λ h, @@mem_ess_image_of_unit_is_iso _ _ _ X h.1⟩
 
-instance is_affine_AffineScheme (X : AffineScheme.{u}) : is_affine (X : Scheme.{u}) :=
-(mem_AffineScheme _).mp X.prop
+instance is_affine_AffineScheme (X : AffineScheme.{u}) : is_affine X.obj :=
+⟨functor.ess_image.unit_is_iso X.property⟩
 
 instance Spec_is_affine (R : CommRingᵒᵖ) : is_affine (Scheme.Spec.obj R) :=
-(mem_AffineScheme _).mp (Scheme.Spec.obj_mem_ess_image R)
+algebraic_geometry.is_affine_AffineScheme ⟨_, Scheme.Spec.obj_mem_ess_image R⟩
 
 lemma is_affine_of_iso {X Y : Scheme} (f : X ⟶ Y) [is_iso f] [h : is_affine Y] :
   is_affine X :=
-by { rw [← mem_AffineScheme] at h ⊢, exact functor.ess_image.of_iso (as_iso f).symm h }
+by { rw [← mem_Spec_ess_image] at h ⊢, exact functor.ess_image.of_iso (as_iso f).symm h }
 
 namespace AffineScheme
 

src/algebraic_geometry/properties.lean

@@ -34,7 +34,7 @@ begin
   rw t0_space_iff_inseparable,
   intros x y h,
   obtain ⟨U, R, ⟨e⟩⟩ := X.local_affine x,
-  have hy : y ∈ U.val := (h.mem_open_iff U.1.2).1 U.2,
+  have hy : y ∈ U.obj := (h.mem_open_iff U.1.2).1 U.2,
   erw ← subtype_inseparable_iff (⟨x, U.2⟩ : U.1.1) (⟨y, hy⟩ : U.1.1) at h,
   let e' : U.1 ≃ₜ prime_spectrum R :=
     homeo_of_iso ((LocallyRingedSpace.forget_to_SheafedSpace ⋙ SheafedSpace.forget _).map_iso e),

src/algebraic_topology/simplex_category.lean

@@ -382,7 +382,7 @@ def is_skeleton_of : is_skeleton_of NonemptyFinLinOrd simplex_category skeletal_
 
 /-- The truncated simplex category. -/
 @[derive small_category]
-def truncated (n : ℕ) := {a : simplex_category // a.len ≤ n}
+def truncated (n : ℕ) := full_subcategory (λ a : simplex_category, a.len ≤ n)
 
 namespace truncated
 

src/category_theory/adjunction/reflective.lean

@@ -156,17 +156,19 @@ by rw [←equiv.eq_symm_apply, unit_comp_partial_bijective_symm_natural A h, equ
 /-- If `i : D ⥤ C` is reflective, the inverse functor of `i ≌ F.ess_image` can be explicitly
 defined by the reflector. -/
 @[simps]
-def equiv_ess_image_of_reflective [reflective i] : D ≌ i.ess_image :=
+def equiv_ess_image_of_reflective [reflective i] : D ≌ i.ess_image_subcategory :=
 { functor := i.to_ess_image,
   inverse := i.ess_image_inclusion ⋙ (left_adjoint i : _),
   unit_iso := nat_iso.of_components (λ X, (as_iso $ (of_right_adjoint i).counit.app X).symm)
     (by { intros X Y f, dsimp, simp only [is_iso.eq_inv_comp, is_iso.comp_inv_eq, category.assoc],
       exact ((of_right_adjoint i).counit.naturality _).symm }),
-  counit_iso := nat_iso.of_components
-    (λ X, by { refine (iso.symm $ as_iso _), exact (of_right_adjoint i).unit.app X,
+  counit_iso :=
+  nat_iso.of_components
+    (λ X, by { refine (iso.symm $ as_iso _), exact (of_right_adjoint i).unit.app X.obj,
       apply_with (is_iso_of_reflects_iso _ i.ess_image_inclusion) { instances := ff },
-      exact functor.ess_image.unit_is_iso X.prop })
-    (by { intros X Y f, dsimp, simp only [is_iso.eq_inv_comp, is_iso.comp_inv_eq, category.assoc],
-      exact ((of_right_adjoint i).unit.naturality f).symm }) }
+      exact functor.ess_image.unit_is_iso X.property })
+    (by { intros X Y f, dsimp, rw [is_iso.comp_inv_eq, assoc],
+      have h := ((of_right_adjoint i).unit.naturality f).symm,
+      rw [functor.id_map] at h, erw [← h, is_iso.inv_hom_id_assoc, functor.comp_map] }) }
 
 end category_theory

src/category_theory/concrete_category/basic.lean

@@ -171,11 +171,11 @@ instance induced_category.has_forget₂ {C : Type v} {D : Type v'} [category D]
   forget_comp := rfl }
 
 instance full_subcategory.concrete_category {C : Type v} [category C] [concrete_category C]
-  (Z : C → Prop) : concrete_category {X : C // Z X} :=
+  (Z : C → Prop) : concrete_category (full_subcategory Z) :=
 { forget := full_subcategory_inclusion Z ⋙ forget C }
 
 instance full_subcategory.has_forget₂ {C : Type v} [category C] [concrete_category C]
-  (Z : C → Prop) : has_forget₂ {X : C // Z X} C :=
+  (Z : C → Prop) : has_forget₂ (full_subcategory Z) C :=
 { forget₂ := full_subcategory_inclusion Z,
   forget_comp := rfl }
 

src/category_theory/connected_components.lean

@@ -41,7 +41,7 @@ instance [inhabited J] : inhabited (connected_components J) := ⟨quotient.mk' d
 
 /-- Given an index for a connected component, produce the actual component as a full subcategory. -/
 @[derive category]
-def component (j : connected_components J) : Type u₁ := {k : J // quotient.mk' k = j}
+def component (j : connected_components J) : Type u₁ := full_subcategory (λ k, quotient.mk' k = j)
 
 /-- The inclusion functor from a connected component to the whole category. -/
 @[derive [full, faithful], simps {rhs_md := semireducible}]
@@ -82,7 +82,7 @@ begin
   { refine @@list.chain_pmap_of_chain _ _ _ f (λ x y _ _ h, _) hl₁ h₁₂ _,
     exact zag_of_zag_obj (component.ι _) h },
   { erw list.last_pmap _ f (j₁ :: l) (by simpa [h₁₂] using hf) (list.cons_ne_nil _ _),
-    exact subtype.ext hl₂ },
+    exact full_subcategory.ext _ _ hl₂ },
 end
 
 /--

src/category_theory/essential_image.lean

@@ -66,21 +66,22 @@ set.ext $ λ A, ⟨ess_image.of_nat_iso h, ess_image.of_nat_iso h.symm⟩
 /-- An object in the image is in the essential image. -/
 lemma obj_mem_ess_image (F : D ⥤ C) (Y : D) : F.obj Y ∈ ess_image F := ⟨Y, ⟨iso.refl _⟩⟩
 
-instance : category F.ess_image := category_theory.full_subcategory _
+/-- The essential image of a functor, interpreted of a full subcategory of the target category. -/
+@[derive category, nolint has_nonempty_instance]
+def ess_image_subcategory (F : C ⥤ D) := full_subcategory F.ess_image
 
 /-- The essential image as a subcategory has a fully faithful inclusion into the target category. -/
 @[derive [full, faithful], simps]
-def ess_image_inclusion (F : C ⥤ D) : F.ess_image ⥤ D :=
+def ess_image_inclusion (F : C ⥤ D) : F.ess_image_subcategory ⥤ D :=
 full_subcategory_inclusion _
 
 /--
 Given a functor `F : C ⥤ D`, we have an (essentially surjective) functor from `C` to the essential
 image of `F`.
 -/
 @[simps]
-def to_ess_image (F : C ⥤ D) : C ⥤ F.ess_image :=
-{ obj := λ X, ⟨_, obj_mem_ess_image _ X⟩,
-  map := λ X Y f, (ess_image_inclusion F).preimage (F.map f) }
+def to_ess_image (F : C ⥤ D) : C ⥤ F.ess_image_subcategory :=
+full_subcategory.lift _ F (obj_mem_ess_image _)
 
 /--
 The functor `F` factorises through its essential image, where the first functor is essentially
@@ -89,7 +90,7 @@ surjective and the second is fully faithful.
 @[simps]
 def to_ess_image_comp_essential_image_inclusion (F : C ⥤ D) :
   F.to_ess_image ⋙ F.ess_image_inclusion ≅ F :=
-nat_iso.of_components (λ X, iso.refl _) (by tidy)
+full_subcategory.lift_comp_inclusion _ _ _
 
 end functor
 

src/category_theory/full_subcategory.lean

@@ -81,35 +81,41 @@ variables {C : Type u₁} [category.{v} C]
 variables (Z : C → Prop)
 
 /--
-The category structure on a subtype; morphisms just ignore the property.
+A subtype-like structure for full subcategories. Morphisms just ignore the property. We don't use
+actual subtypes since the simp-normal form `↑X` of `X.val` does not work well for full
+subcategories.
 
 See <https://stacks.math.columbia.edu/tag/001D>. We do not define 'strictly full' subcategories.
 -/
-instance full_subcategory : category.{v} {X : C // Z X} :=
-induced_category.category subtype.val
+@[ext, nolint has_nonempty_instance] structure full_subcategory :=
+(obj : C)
+(property : Z obj)
+
+instance full_subcategory.category : category.{v} (full_subcategory Z) :=
+induced_category.category full_subcategory.obj
 
 /--
 The forgetful functor from a full subcategory into the original category
 ("forgetting" the condition).
 -/
-def full_subcategory_inclusion : {X : C // Z X} ⥤ C :=
-induced_functor subtype.val
+def full_subcategory_inclusion : full_subcategory Z ⥤ C :=
+induced_functor full_subcategory.obj
 
 @[simp] lemma full_subcategory_inclusion.obj {X} :
-  (full_subcategory_inclusion Z).obj X = X.val := rfl
+  (full_subcategory_inclusion Z).obj X = X.obj := rfl
 @[simp] lemma full_subcategory_inclusion.map {X Y} {f : X ⟶ Y} :
   (full_subcategory_inclusion Z).map f = f := rfl
 
 instance full_subcategory.full : full (full_subcategory_inclusion Z) :=
-induced_category.full subtype.val
+induced_category.full _
 instance full_subcategory.faithful : faithful (full_subcategory_inclusion Z) :=
-induced_category.faithful subtype.val
+induced_category.faithful _
 
 variables {Z} {Z' : C → Prop}
 
 /-- An implication of predicates `Z → Z'` induces a functor between full subcategories. -/
 @[simps]
-def full_subcategory.map (h : ∀ ⦃X⦄, Z X → Z' X) : {X // Z X} ⥤ {X // Z' X} :=
+def full_subcategory.map (h : ∀ ⦃X⦄, Z X → Z' X) : full_subcategory Z ⥤ full_subcategory Z' :=
 { obj := λ X, ⟨X.1, h X.2⟩,
   map := λ X Y f, f }
 
@@ -128,7 +134,7 @@ variables {D : Type u₂} [category.{v₂} D] (P Q : D → Prop)
 /-- A functor which maps objects to objects satisfying a certain property induces a lift through
     the full subcategory of objects satisfying that property. -/
 @[simps]
-def full_subcategory.lift (F : C ⥤ D) (hF : ∀ X, P (F.obj X)) : C ⥤ {X // P X} :=
+def full_subcategory.lift (F : C ⥤ D) (hF : ∀ X, P (F.obj X)) : C ⥤ full_subcategory P :=
 { obj := λ X, ⟨F.obj X, hF X⟩,
   map := λ X Y f, F.map f }
 

src/category_theory/monoidal/subcategory.lean

@@ -45,11 +45,11 @@ open monoidal_predicate
 variables [monoidal_predicate P]
 
 /--
-When `P` is a monoidal predicate, the full subcategory `{X : C // P X}` inherits the monoidal
-structure of `C`
+When `P` is a monoidal predicate, the full subcategory for `P` inherits the monoidal structure of
+  `C`.
 -/
-instance full_monoidal_subcategory : monoidal_category {X : C // P X} :=
-{ tensor_obj := λ X Y, ⟨X ⊗ Y, prop_tensor X.2 Y.2⟩,
+instance full_monoidal_subcategory : monoidal_category (full_subcategory P) :=
+{ tensor_obj := λ X Y, ⟨X.1 ⊗ Y.1, prop_tensor X.2 Y.2⟩,
   tensor_hom := λ X₁ Y₁ X₂ Y₂ f g, by { change X₁.1 ⊗ X₂.1 ⟶ Y₁.1 ⊗ Y₂.1,
     change X₁.1 ⟶ Y₁.1 at f, change X₂.1 ⟶ Y₂.1 at g, exact f ⊗ g },
   tensor_unit := ⟨𝟙_ C, prop_id⟩,
@@ -71,7 +71,7 @@ The forgetful monoidal functor from a full monoidal subcategory into the origina
 ("forgetting" the condition).
 -/
 @[simps]
-def full_monoidal_subcategory_inclusion : monoidal_functor {X : C // P X} C :=
+def full_monoidal_subcategory_inclusion : monoidal_functor (full_subcategory P) C :=
 { to_functor := full_subcategory_inclusion P,
   ε := 𝟙 _,
   μ := λ X Y, 𝟙 _ }
@@ -87,7 +87,7 @@ variables {P} {P' : C → Prop} [monoidal_predicate P']
 subcategories. -/
 @[simps]
 def full_monoidal_subcategory.map (h : ∀ ⦃X⦄, P X → P' X) :
-  monoidal_functor {X : C // P X} {X : C // P' X}  :=
+  monoidal_functor (full_subcategory P) (full_subcategory P')  :=
 { to_functor := full_subcategory.map h,
   ε := 𝟙 _,
   μ := λ X Y, 𝟙 _ }
@@ -102,9 +102,9 @@ section braided
 variables (P) [braided_category C]
 
 /--
-The braided structure on `{X : C // P X}` inherited by the braided structure on `C`.
+The braided structure on a full subcategory inherited by the braided structure on `C`.
 -/
-instance full_braided_subcategory : braided_category {X : C // P X} :=
+instance full_braided_subcategory : braided_category (full_subcategory P) :=
 braided_category_of_faithful (full_monoidal_subcategory_inclusion P)
   (λ X Y, ⟨(β_ X.1 Y.1).hom, (β_ X.1 Y.1).inv, (β_ X.1 Y.1).hom_inv_id, (β_ X.1 Y.1).inv_hom_id⟩)
   (λ X Y, by tidy)
@@ -114,7 +114,7 @@ The forgetful braided functor from a full braided subcategory into the original
 ("forgetting" the condition).
 -/
 @[simps]
-def full_braided_subcategory_inclusion : braided_functor {X : C // P X} C :=
+def full_braided_subcategory_inclusion : braided_functor (full_subcategory P) C :=
 { to_monoidal_functor := full_monoidal_subcategory_inclusion P,
   braided' := λ X Y, by { rw [is_iso.eq_inv_comp], tidy } }
 
@@ -129,7 +129,7 @@ variables {P}
 subcategories. -/
 @[simps]
 def full_braided_subcategory.map (h : ∀ ⦃X⦄, P X → P' X) :
-  braided_functor {X : C // P X} {X : C // P' X}  :=
+  braided_functor (full_subcategory P) (full_subcategory P')  :=
 { to_monoidal_functor := full_monoidal_subcategory.map h,
   braided' := λ X Y, by { rw [is_iso.eq_inv_comp], tidy }  }
 
@@ -144,7 +144,7 @@ section symmetric
 
 variables (P) [symmetric_category C]
 
-instance full_symmetric_subcategory : symmetric_category {X : C // P X} :=
+instance full_symmetric_subcategory : symmetric_category (full_subcategory P) :=
 symmetric_category_of_faithful (full_braided_subcategory_inclusion P)
 
 end symmetric

src/category_theory/preadditive/additive_functor.lean

@@ -147,7 +147,7 @@ variables (C D : Type*) [category C] [category D] [preadditive C] [preadditive D
 /-- Bundled additive functors. -/
 @[derive category, nolint has_nonempty_instance]
 def AdditiveFunctor :=
-{ F : C ⥤ D // functor.additive F }
+full_subcategory (λ (F : C ⥤ D), F.additive)
 
 infixr ` ⥤+ `:26 := AdditiveFunctor
 

src/category_theory/sites/sieves.lean

@@ -44,7 +44,7 @@ instance : inhabited (presieve X) := ⟨⊤⟩
 /-- Given a sieve `S` on `X : C`, its associated diagram `S.diagram` is defined to be
     the natural functor from the full subcategory of the over category `C/X` consisting
     of arrows in `S` to `C`. -/
-abbreviation diagram (S : presieve X) : {f : over X // S f.hom} ⥤ C :=
+abbreviation diagram (S : presieve X) : full_subcategory (λ (f : over X), S f.hom) ⥤ C :=
 full_subcategory_inclusion _ ⋙ over.forget X
 
 /-- Given a sieve `S` on `X : C`, its associated cocone `S.cocone` is defined to be