-- Lattice homomorphisms
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Lattice.LatticeHom
import Monotone

predicate IsLatticeHom (f A r B s : Set) :=
  IsLattice(A, r) ∧ IsLattice(B, s) ∧ FunctionBetween(f, A, B) ∧
  (∀ x ∈ A, ∀ y ∈ A, f(join(A, r, x, y)) = join(B, s, f(x), f(y))) ∧
  (∀ x ∈ A, ∀ y ∈ A, f(meet(A, r, x, y)) = meet(B, s, f(x), f(y)))

theorem IsLatticeHom.source (f A r B s : Set)
  requires h : IsLatticeHom(f, A, r, B, s)
  shows IsLattice(A, r)
proof
  simp [IsLatticeHom]

theorem IsLatticeHom.target (f A r B s : Set)
  requires h : IsLatticeHom(f, A, r, B, s)
  shows IsLattice(B, s)
proof
  simp [IsLatticeHom]

theorem IsLatticeHom.function (f A r B s : Set)
  requires h : IsLatticeHom(f, A, r, B, s)
  shows f : A → B
proof
  simp [IsLatticeHom]

theorem IsLatticeHom.join (f A r B s x y : Set)
  requires h : IsLatticeHom(f, A, r, B, s)
  requires hx : x ∈ A
  requires hy : y ∈ A
  shows f(join(A, r, x, y)) = join(B, s, f(x), f(y))
proof
  rcases h with ⟨source, target, function, joins, meets⟩
  exact joins with x, hx, y, hy

theorem IsLatticeHom.meet (f A r B s x y : Set)
  requires h : IsLatticeHom(f, A, r, B, s)
  requires hx : x ∈ A
  requires hy : y ∈ A
  shows f(meet(A, r, x, y)) = meet(B, s, f(x), f(y))
proof
  rcases h with ⟨source, target, function, joins, meets⟩
  exact meets with x, hx, y, hy

theorem IsLatticeHom.apply_member (f A r B s x : Set)
  requires h : IsLatticeHom(f, A, r, B, s)
  requires hx : x ∈ A
  shows f(x) ∈ B
proof
  exact FunctionBetween.apply_closed with (IsLatticeHom.function with h), hx

theorem IsLatticeHom.monotone (f A r B s : Set)
  requires h : IsLatticeHom(f, A, r, B, s)
  shows IsMonotoneMap(f, A, r, B, s)
proof
  have source := IsLatticeHom.source with h
  have target := IsLatticeHom.target with h
  constructor
  . exact IsLatticeHom.function with h
  . intros x hx y hy hxy
    have fxB := IsLatticeHom.apply_member with h, hx
    have fyB := IsLatticeHom.apply_member with h, hy
    have joined := join.of_le with source, hx, hy, hxy
    have preserved := IsLatticeHom.join with h, hx, hy
    rw joined at preserved
    symm at preserved
    exact join.eq_right_iff.backward with target, fxB, fyB, preserved

theorem IsLatticeHom.identity (A r : Set)
  requires lattice : IsLattice(A, r)
  shows IsLatticeHom(identity(A), A, r, A, r)
proof
  refine ⟨lattice, lattice, identity.function at A, ?_, ?_⟩
  . intros x hx y hy
    have valueX := identity.apply with hx
    have valueY := identity.apply with hy
    have valueJoin := identity.apply with (join.member with lattice, hx, hy)
    rw [valueX, valueY, valueJoin]
    rfl
  . intros x hx y hy
    have valueX := identity.apply with hx
    have valueY := identity.apply with hy
    have valueMeet := identity.apply with (meet.member with lattice, hx, hy)
    rw [valueX, valueY, valueMeet]
    rfl

theorem IsLatticeHom.compose (f g A r B s C t : Set)
  requires hf : IsLatticeHom(f, A, r, B, s)
  requires hg : IsLatticeHom(g, B, s, C, t)
  shows IsLatticeHom(compose(g, f, A, B, C), A, r, C, t)
proof
  have source := IsLatticeHom.source with hf
  have middle := IsLatticeHom.target with hf
  have target := IsLatticeHom.target with hg
  have fFunction := IsLatticeHom.function with hf
  have gFunction := IsLatticeHom.function with hg
  refine ⟨source, target, (compose.function with fFunction, gFunction), ?_, ?_⟩
  . intros x hx y hy
    have joinA := join.member with source, hx, hy
    have fxB := IsLatticeHom.apply_member with hf, hx
    have fyB := IsLatticeHom.apply_member with hf, hy
    have valueX := compose.apply with fFunction, gFunction, hx
    have valueY := compose.apply with fFunction, gFunction, hy
    have valueJoin := compose.apply with fFunction, gFunction, joinA
    have innerJoin := IsLatticeHom.join with hf, hx, hy
    have outerJoin := IsLatticeHom.join with hg, fxB, fyB
    rw [valueX, valueY, valueJoin, innerJoin]
    exact outerJoin
  . intros x hx y hy
    have meetA := meet.member with source, hx, hy
    have fxB := IsLatticeHom.apply_member with hf, hx
    have fyB := IsLatticeHom.apply_member with hf, hy
    have valueX := compose.apply with fFunction, gFunction, hx
    have valueY := compose.apply with fFunction, gFunction, hy
    have valueMeet := compose.apply with fFunction, gFunction, meetA
    have innerMeet := IsLatticeHom.meet with hf, hx, hy
    have outerMeet := IsLatticeHom.meet with hg, fxB, fyB
    rw [valueX, valueY, valueMeet, innerMeet]
    exact outerMeet

-- An order isomorphism between lattices preserves joins and meets.

theorem OrderIsomorphism.join (f A r B s x y : Set)
  requires h : OrderIsomorphism(f, A, r, B, s)
  requires source : IsLattice(A, r)
  requires target : IsLattice(B, s)
  requires hx : x ∈ A
  requires hy : y ∈ A
  shows f(join(A, r, x, y)) = join(B, s, f(x), f(y))
proof
  have embedding := OrderIsomorphism.embedding with h
  have monotone := OrderEmbedding.monotone with embedding
  have surjective := Bijective.surjective with
      (OrderIsomorphism.bijective with h)
  have joinA := join.member with source, hx, hy
  have fxB := IsMonotoneMap.apply_member with monotone, hx
  have fyB := IsMonotoneMap.apply_member with monotone, hy
  have fJ := IsMonotoneMap.apply_member with monotone, joinA
  have xJ := IsMonotoneMap.preserves with monotone, hx, joinA,
      (join.upper_left with source, hx, hy)
  have yJ := IsMonotoneMap.preserves with monotone, hy, joinA,
      (join.upper_right with source, hx, hy)
  have supremum : Supremum(B, s, {f(x), f(y)}, f(join(A, r, x, y)))
    apply Supremum.of_pair with fxB, fyB, fJ, xJ, yJ
    intros b hb xb yb
    rcases surjective with ⟨function, onto⟩
    obtain ⟨a, ha, mapped⟩ := onto with b, hb
    have value := FunctionBetween.apply_value with function, ha, mapped
    rw ← value at xb
    rw ← value at yb
    rw ← value
    have xa := OrderEmbedding.reflects with embedding, hx, ha, xb
    have ya := OrderEmbedding.reflects with embedding, hy, ha, yb
    have below := join.least with source, hx, hy, ha, xa, ya
    exact IsMonotoneMap.preserves with monotone, joinA, ha, below
  exact join.of_supremum with target, fxB, fyB, supremum

theorem OrderIsomorphism.meet (f A r B s x y : Set)
  requires h : OrderIsomorphism(f, A, r, B, s)
  requires source : IsLattice(A, r)
  requires target : IsLattice(B, s)
  requires hx : x ∈ A
  requires hy : y ∈ A
  shows f(meet(A, r, x, y)) = meet(B, s, f(x), f(y))
proof
  have embedding := OrderIsomorphism.embedding with h
  have monotone := OrderEmbedding.monotone with embedding
  have surjective := Bijective.surjective with
      (OrderIsomorphism.bijective with h)
  have meetA := meet.member with source, hx, hy
  have fxB := IsMonotoneMap.apply_member with monotone, hx
  have fyB := IsMonotoneMap.apply_member with monotone, hy
  have fM := IsMonotoneMap.apply_member with monotone, meetA
  have mX := IsMonotoneMap.preserves with monotone, meetA, hx,
      (meet.lower_left with source, hx, hy)
  have mY := IsMonotoneMap.preserves with monotone, meetA, hy,
      (meet.lower_right with source, hx, hy)
  have infimum : Infimum(B, s, {f(x), f(y)}, f(meet(A, r, x, y)))
    apply Infimum.of_pair with fxB, fyB, fM, mX, mY
    intros b hb bx byBound
    rcases surjective with ⟨function, onto⟩
    obtain ⟨a, ha, mapped⟩ := onto with b, hb
    have value := FunctionBetween.apply_value with function, ha, mapped
    rw ← value at bx
    rw ← value at byBound
    rw ← value
    have ax := OrderEmbedding.reflects with embedding, ha, hx, bx
    have ay := OrderEmbedding.reflects with embedding, ha, hy, byBound
    have above := meet.greatest with source, hx, hy, ha, ax, ay
    exact IsMonotoneMap.preserves with monotone, ha, meetA, above
  exact meet.of_infimum with target, fxB, fyB, infimum

theorem OrderIsomorphism.lattice_hom (f A r B s : Set)
  requires h : OrderIsomorphism(f, A, r, B, s)
  requires source : IsLattice(A, r)
  requires target : IsLattice(B, s)
  shows IsLatticeHom(f, A, r, B, s)
proof
  have function := Injective.function with
      (Bijective.injective with (OrderIsomorphism.bijective with h))
  refine ⟨source, target, function, ?_, ?_⟩
  . intros x hx y hy
    exact OrderIsomorphism.join with h, source, target, hx, hy
  . intros x hx y hy
    exact OrderIsomorphism.meet with h, source, target, hx, hy