Image of a FrameHom is a Frame

Stream: Is there code for X?

[Christian K]

Hi there,
I have a FrameHom f between two Frames X and Y. (I know about the Frame structure of X and Y). However, f does not hit every element of Y. This means that the subset of Y, Z = Set.range f which is hit by f, has it's own Frame Structure (right?). Is there something in mathlib with which I can aquire this Frame Structure of Z? If not, should this be something that is in mathlib?

[Yaël Dillies]

We don't have that. It should probably be stated in terms of subframes, which we don't have either

[Christian K]

Wouldn't a subframe be the same thing as a complete sublattice (except for having instFrame)?
(Because a subframe is just a subset of a Frame which is closed under suprema und infima, which is the same thing as a completesublattice, with the only difference being the structure of the parent (frame/completeLattice))

[Yaël Dillies]

I haven't thought very much about subframes, but yes this sounds plausible

[Christian K]

Does it make sense to have something like this in mathlib for subframes?

import Mathlib.Order.CompleteSublattice
import Mathlib.Order.CompleteLattice
import Mathlib.Tactic


variable (α : Type*) [Order.Frame α]

abbrev Subframe := @CompleteSublattice α _


variable (S : Subframe α)

def minAx2 : Order.Frame.MinimalAxioms α where
  inf_sSup_le_iSup_inf := Order.Frame.inf_sSup_le_iSup_inf

def minAx : Order.Frame.MinimalAxioms S :=
  Subtype.coe_injective.frameMinimalAxioms (minAx2 α) _ (fun _ _ ↦ rfl)
  (fun _ _ ↦ rfl) CompleteSublattice.coe_sSup'
  CompleteSublattice.coe_sInf' (rfl) (rfl)


instance instFrame : Order.Frame S :=
  Order.Frame.ofMinimalAxioms (minAx α S)

[Yaël Dillies]

I think you can skip defining Subframe

[Christian K]

Ok, I created a pr for further discussion

[Christian K]

Christian K said:

Hi there,
I have a FrameHom f between two Frames X and Y. (I know about the Frame structure of X and Y). However, f does not hit every element of Y. This means that the subset of Y, Z = Set.range f which is hit by f, has it's own Frame Structure (right?). Is there something in mathlib with which I can aquire this Frame Structure of Z? If not, should this be something that is in mathlib?

Wait, this is not even true, a FrameHom only preserves finite intersections and arbitrary suprema, I would need a CompleteLatticeHom which also preserves arbitrary intersections.