Good tips for subalgebras

Stream: Berkeley Lean Seminar

[Kentarô YAMAMOTO]

I use lattices as an example, but I believe that this issue arises with any algebraic structure. Assume that I have shown that the family of compact open sets of a topological space is a bounded lattice:

namespace compact_opens
def compact_open_sets (α : Type u) [topological_space α] : set (set α) :=
  λ U, is_open U ∧ compact U
def compact_opens (α : Type u) [topological_space α] :=
  { U : opens α // @compact_open_sets α _ U }
instance {α : Type u} [topological_space α] : bounded_lattice (compact_opens α) := sorry
end topological_space

I also have a type class that adds new data to topological spaces:

class toporthoframe (α : Type u) extends orthoframe α, topological_space α := mk

where orthoframe yet another type class. Now I consider a subtype of compact_opens:

def compact_open_perp_regular_set (α : Type u) [toporthoframe α] : set (set α) :=
  { U ∈ topological_space.compact_open_sets α | sorry }

def compact_opens_perp_regular (α : Type u) [toporthoframe α] :=
  { U : topological_space.compact_opens α //  (↑U : set α) ∈ compact_open_perp_regular_set α}

I want to define an instance of bounded_lattice for compact_opens_perp_regular that is a subalgebra of compact_opens.

I am sure that this is a recurrent pattern in algebra. What is an efficient way of defining such an instance without defining a dozen properties for bounded_lattice?

[Patrick Lutz]

I would try asking on the #new members or #general streams

[Kevin Buzzard]

You can maybe pull lattice structures back; you might want to see if there's something called lattice.comap, that's probably what the construction will be called