Subobjects of quotients

Stream: general

[Peter Nelson]

The following code gives a simple example of a structure Foo, together with a quotient and a subobject. Mathematically, the subobject and quotient should combine in a natural way to give a notion of subFoo_quot, but I can't seem to figure out how to write code that corresponds to this, in a way where this notion interacts naturally with both subFoo and Foo_quot. Can anyone help with this?

variables {α : Type}

structure Foo (α : Type) :=
(f : α → ℤ)

def r : Foo α → Foo α → Prop := λ S S', ∀ a, (S.f a = S'.f a) ∨ (S.f a = - S'.f a)

lemma is_equivalence : equivalence (r : Foo α → Foo α → Prop) := sorry
-- easy

instance Foo_setoid (α : Type) : setoid (Foo α) :=
  setoid.mk _ is_equivalence

def Foo_quot (α : Type) := quotient (Foo_setoid α)

structure subFoo (F : Foo α) :=
(carrier : set α)

[Kevin Buzzard]

I'm not sure I understand the question. If f : X -> Y is a function between types (for example quotient.mk) then set.image f : set X -> set Y is the induced function from subsets of X to subsets of Y. Is this what you're after?

[Peter Nelson]

I think I've oversimplified the question. Suppose that I add the following.

structure small_set_in_Foo (F : Foo α) :=
(carrier : set α)
(small : ∀ a, a ∈ carrier → (F.f a)*(F.f a) < 100)

Then mathematically, small_set_in_Foo F is a set in α that F.f sends to small values. The definition of small_set_in_Foo is invariant under the equivalence relation r, so there should be a corresponding small_set_in_Foo_quot (Fq : Foo_quot) structure corresponding to a set in α whose elements are sent to small values by Fq, and also, results about small_set_in_Foo F should imply things about small_set_in_Foo_quot ⟦F⟧. But the usual quot.lift_on way to transfer a definition to the quotient won't work here, because small_set_in_Foo is a Pi type on Foo rather than just a function on Foo. So how should one talk about this structure?

Does this make sense?