Unbounded lattice homomorphisms #
This file defines unbounded lattice homomorphisms. Bounded lattice homomorphisms are defined in
Mathlib/Order/Hom/BoundedLattice.lean
.
We use the DFunLike
design, so each type of morphisms has a companion typeclass which is meant to
be satisfied by itself and all stricter types.
Types of morphisms #
SupHom
: Maps which preserve⊔
.InfHom
: Maps which preserve⊓
.LatticeHom
: Lattice homomorphisms. Maps which preserve⊔
and⊓
.
Typeclasses #
The type of ⊔
-preserving functions from α
to β
.
- toFun : α → β
Instances For
The type of ⊓
-preserving functions from α
to β
.
- toFun : α → β
Instances For
The type of lattice homomorphisms from α
to β
.
- toFun : α → β
A
LatticeHom
preserves infima.Do not use this directly. Use
map_inf
instead.
Instances For
SupHomClass F α β
states that F
is a type of ⊔
-preserving morphisms.
You should extend this class when you extend SupHom
.
A
SupHomClass
morphism preserves suprema.
Instances
InfHomClass F α β
states that F
is a type of ⊓
-preserving morphisms.
You should extend this class when you extend InfHom
.
An
InfHomClass
morphism preserves infima.
Instances
LatticeHomClass F α β
states that F
is a type of lattice morphisms.
You should extend this class when you extend LatticeHom
.
A
LatticeHomClass
morphism preserves infima.
Instances
We can regard an injective map preserving binary infima as an order embedding.
Equations
Instances For
Equations
Supremum homomorphisms #
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Subtype.val
as a SupHom
.
Equations
Instances For
Infimum homomorphisms #
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Subtype.val
as an InfHom
.
Equations
Instances For
Lattice homomorphisms #
Reinterpret a LatticeHom
as an InfHom
.
Equations
Instances For
Equations
Copy of a LatticeHom
with a new toFun
equal to the old one. Useful to fix definitional
equalities.
Equations
Instances For
Equations
Composition of LatticeHom
s as a LatticeHom
.
Equations
Instances For
Subtype.val
as a LatticeHom
.
Equations
Instances For
An order homomorphism from a linear order is a lattice homomorphism.
Reinterpret an order homomorphism to a linear order as a LatticeHom
.
Equations
Instances For
Dual homs #
Reinterpret a lattice homomorphism as a lattice homomorphism between the dual lattices.
Equations
Instances For
Prod #
Natural projection homomorphism from α × β
to α
.
Equations
Instances For
Natural projection homomorphism from α × β
to β
.
Equations
Instances For
Pi #
Evaluation as a lattice homomorphism.