There seems to be conflicting information about frames and complete Heyting algebras. Everyone seems to agree on the fact that frames are lattices in which any subset has a supremum, but not every source seems to agree wether only finite infimums have to exist or infinite as well. Any topology can be made into a frame by the usual union=supremum, intersection=infimum. That begs the question what an infinite infimum would look like in such a frame induced by a topology.
On the other hand, there is no confusion that complete Heyting algebras are complete lattices, i.e. any subset must have a supremum and infimum. Now the funny part is that the category of frames and the category of complete Heyting algebras have the same objects.
So how does this work? Do frames have to be complete as well then? And why is this sometimes not in the definition?
To show some sources:
Everybody agrees that complete Heyting algebras are complete lattices, i.e. all subsets have both a supremum and an infimum.
There is some confusion about when complete Heyting algebras and frames are the same, however:
- "Complete Heyting algebras are the objects of three different categories; the category CHey, the category Loc of locales, and its opposite, the category Frm of frames." – Wikipedia
- "Also, when considering large lattices which are only small-complete, then frames and complete Heyting algebras are different objects." – nLab
- "A complete Heyting algebra is also called a frame." – PlanetMath
- " frame 𝒪 is a poset that has all small coproducts, called joins (⋁) and all finite limits, called meets (∧) and which satisfies the infinite distributive law." – nLab
- "Formally, a locale is a complete lattice L that is meet infinitely distributive. (…) A locale is also called a frame (…) " – PlanetMath
In most documents I found, the definition for frame was indeed one where only finite meets have to exist.
Best Answer
So the thing is that frames are the same thing as complete Heyting algebras in terms of objects; but they have different names because of the morphisms.
In particular their description is different because it stresses what those morphisms are expected to preserve.
In particular for frames, we say they have arbitrary joins, finite meets which distribute over the joins; and so implicitly we are saying that a frame morphism is a lattice morphism that preserves arbitrary joind and finite meets; whereas for Heyting algebras we are insisting on the $\implies$ operation, which means implicitly that the morphisms should preserve this.
So even though arbitrary meets do exist in a frame (you can prove that a poset has all joins iff it has all meets), not mentioning them means they are not expected to be preserved under the morphisms. In the example of a topology, the one you mentioned, this is because a finite meet is just an intersection, which is preserved under $f^{-1}$ for $f$ a map, whereas an infinite meet is the interior of that intersection, which need not be preserved under $f^{-1}$ even if $f$ is continuous.