Lumenary.StructurePreservingMaps

Formal library

• PreservesOpdefDefinitionNo axioms

  /-- `PreservesOp f opA opB` says that `f : A → B` **preserves the operation**: combining first
  and then mapping gives the same as mapping first and then combining,
  `f (x ∗ y) = f x ⋆ f y` for all `x y`, where `∗` is `opA` and `⋆` is `opB`. -/
  def PreservesOp {A : Type u} {B : Type v} (f : A → B) (opA : A → A → A) (opB : B → B → B) :
      Prop :=
    ∀ x y, f (opA x y) = opB (f x) (f y)

  Axioms used: No axiomsformal/Lumenary/StructurePreservingMaps.leanTry it in the Lean web editor

• preservesOp_idtheoremProved here from basic factsNo axioms

  /-- The identity map preserves every operation: both sides are `x ∗ y`. -/
  theorem preservesOp_id {A : Type u} (op : A → A → A) : PreservesOp id op op :=
    fun _ _ => rfl

  Axioms used: No axiomsformal/Lumenary/StructurePreservingMaps.leanTry it in the Lean web editor

• PreservesOp.comptheoremProved here from basic factsNo axioms

  /-- **Composites of homomorphisms are homomorphisms.** If `f` turns `∗` into `⋆` and `g` turns
  `⋆` into `•`, then `g ∘ f` turns `∗` into `•`:
  `g(f(x ∗ y)) = g(f x ⋆ f y) = g(f x) • g(f y)`. -/
  theorem PreservesOp.comp {A : Type u} {B : Type v} {C : Type w}
      {opA : A → A → A} {opB : B → B → B} {opC : C → C → C} {f : A → B} {g : B → C}
      (hf : PreservesOp f opA opB) (hg : PreservesOp g opB opC) :
      PreservesOp (g ∘ f) opA opC := by
    intro x y
    calc (g ∘ f) (opA x y) = g (f (opA x y)) := rfl
      _ = g (opB (f x) (f y)) := by rw [hf]
      _ = opC (g (f x)) (g (f y)) := hg _ _

  Axioms used: No axiomsformal/Lumenary/StructurePreservingMaps.leanTry it in the Lean web editor

• PreservesOp.inversetheoremProved here from basic factsNo axioms

  /-- **The inverse of a bijective homomorphism is a homomorphism.** Let `g` be a two-sided inverse
  of `f` (`g (f x) = x` and `f (g u) = u`). For `u v` in `B`, write `u = f (g u)` and
  `v = f (g v)`; then
  `g (u ⋆ v) = g (f (g u) ⋆ f (g v)) = g (f (g u ∗ g v)) = g u ∗ g v`.
  Nothing about groups is used: this holds for any binary operations. -/
  theorem PreservesOp.inverse {A : Type u} {B : Type v} {opA : A → A → A} {opB : B → B → B}
      {f : A → B} {g : B → A} (hf : PreservesOp f opA opB)
      (hgf : Function.LeftInverse g f) (hfg : Function.RightInverse g f) :
      PreservesOp g opB opA := by
    intro u v
    calc g (opB u v) = g (opB (f (g u)) (f (g v))) := by rw [hfg u, hfg v]
      _ = g (f (opA (g u) (g v))) := by rw [hf]
      _ = opA (g u) (g v) := hgf _

  Axioms used: No axiomsformal/Lumenary/StructurePreservingMaps.leanTry it in the Lean web editor

• reduce_addtheoremApplies a library theorempropext, Quot.sound

  /-- Reduction modulo `n`, `ℤ → ℤ/n`, preserves addition. This is core Mathlib's `Int.cast_add`
  (the map `ℤ → ZMod n` is the canonical "cast"). -/
  theorem reduce_add (n : ℕ) : PreservesOp (fun a : ℤ => (a : ZMod n)) (· + ·) (· + ·) :=
    fun a b => Int.cast_add a b

  Axioms used: propext, Quot.soundformal/Lumenary/StructurePreservingMaps.leanTry it in the Lean web editor

• reduce_multheoremApplies a library theorempropext, Quot.sound

  /-- Reduction modulo `n` also preserves multiplication: Mathlib's `Int.cast_mul`. -/
  theorem reduce_mul (n : ℕ) : PreservesOp (fun a : ℤ => (a : ZMod n)) (· * ·) (· * ·) :=
    fun a b => Int.cast_mul a b

  Axioms used: propext, Quot.soundformal/Lumenary/StructurePreservingMaps.leanTry it in the Lean web editor

• reduce_not_injectivetheoremProved here from basic factspropext, Quot.sound

  /-- …but for `n ≠ 0` it is **not injective**: `n` and `0` have the same remainder. So reduction
  mod `n` is a homomorphism, not an isomorphism. -/
  theorem reduce_not_injective (n : ℕ) (hn : n ≠ 0) :
      ¬ Function.Injective (fun a : ℤ => (a : ZMod n)) := by
    intro hinj
    have h : ((n : ℤ) : ZMod n) = ((0 : ℤ) : ZMod n) := by
      rw [Int.cast_natCast, ZMod.natCast_self, Int.cast_zero]
    have h' : (n : ℤ) = 0 := hinj h
    exact hn (by exact_mod_cast h')

  Axioms used: propext, Quot.soundformal/Lumenary/StructurePreservingMaps.leanTry it in the Lean web editor

• map_zero_of_preservesOptheoremProved here from basic factspropext

  /-- An addition-preserving map between additive groups sends `0` to `0`:
  `f 0 + f 0 = f (0 + 0) = f 0 = f 0 + 0`, and cancelling `f 0` gives `f 0 = 0`.
  (Mathlib: `map_zero` for bundled homomorphisms.) -/
  theorem map_zero_of_preservesOp {A : Type u} {B : Type v} [AddGroup A] [AddGroup B] {f : A → B}
      (hf : PreservesOp f (· + ·) (· + ·)) : f 0 = 0 := by
    have h : f 0 + f 0 = f 0 + 0 :=
      calc f 0 + f 0 = f (0 + 0) := (hf 0 0).symm
        _ = f 0 := by rw [add_zero]
        _ = f 0 + 0 := (add_zero _).symm
    exact add_left_cancel h

  Axioms used: propextformal/Lumenary/StructurePreservingMaps.leanTry it in the Lean web editor

• map_neg_of_preservesOptheoremProved here from basic factspropext

  /-- …and it sends negatives to negatives: `f (-x) + f x = f (-x + x) = f 0 = 0`, so
  `f (-x) = -f x`. (Mathlib: `map_neg`.) -/
  theorem map_neg_of_preservesOp {A : Type u} {B : Type v} [AddGroup A] [AddGroup B] {f : A → B}
      (hf : PreservesOp f (· + ·) (· + ·)) (x : A) : f (-x) = -f x := by
    have h : f (-x) + f x = 0 :=
      calc f (-x) + f x = f (-x + x) := (hf (-x) x).symm
        _ = f 0 := by rw [neg_add_cancel]
        _ = 0 := map_zero_of_preservesOp hf
    exact eq_neg_of_add_eq_zero_left h

  Axioms used: propextformal/Lumenary/StructurePreservingMaps.leanTry it in the Lean web editor

• comm_of_surjectivetheoremProved here from basic factsNo axioms

  /-- **Structure transfers along homomorphisms.** If `f` preserves the operation and is
  surjective, and `∗` is commutative, then so is `⋆`: write `u = f x`, `v = f y`; then
  `u ⋆ v = f (x ∗ y) = f (y ∗ x) = v ⋆ u`. In particular isomorphic structures are either both
  commutative or both not. -/
  theorem comm_of_surjective {A : Type u} {B : Type v} {opA : A → A → A} {opB : B → B → B}
      {f : A → B} (hf : PreservesOp f opA opB) (hsurj : Function.Surjective f)
      (hcomm : ∀ x y, opA x y = opA y x) : ∀ u v, opB u v = opB v u := by
    intro u v
    obtain ⟨x, rfl⟩ := hsurj u
    obtain ⟨y, rfl⟩ := hsurj v
    rw [← hf, ← hf, hcomm]

  Axioms used: No axiomsformal/Lumenary/StructurePreservingMaps.leanTry it in the Lean web editor

• exp_preservestheoremApplies a library theorempropext, Classical.choice, Quot.sound

  /-- `exp : (ℝ, +) → (ℝ, ×)` turns sums into products: Mathlib's `Real.exp_add`. -/
  theorem exp_preserves : PreservesOp Real.exp (· + ·) (· * ·) :=
    Real.exp_add

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/StructurePreservingMaps.leanTry it in the Lean web editor

• posMuldefDefinitionpropext, Classical.choice, Quot.sound

  /-- The positive reals `ℝ>0`, as the subtype `{y : ℝ // 0 < y}`, with multiplication
  (a product of positive numbers is positive, `mul_pos`). -/
  def posMul (u v : {y : ℝ // 0 < y}) : {y : ℝ // 0 < y} :=
    ⟨u.1 * v.1, mul_pos u.2 v.2⟩

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/StructurePreservingMaps.leanTry it in the Lean web editor

• expPosdefDefinitionpropext, Classical.choice, Quot.sound

  /-- `exp` as a map `ℝ → ℝ>0` (its values are positive, `Real.exp_pos`). -/
  noncomputable def expPos (x : ℝ) : {y : ℝ // 0 < y} :=
    ⟨Real.exp x, Real.exp_pos x⟩

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/StructurePreservingMaps.leanTry it in the Lean web editor

• logPosdefDefinitionpropext, Classical.choice, Quot.sound

  /-- `ln` as a map `ℝ>0 → ℝ`. -/
  noncomputable def logPos (u : {y : ℝ // 0 < y}) : ℝ :=
    Real.log u.1

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/StructurePreservingMaps.leanTry it in the Lean web editor

• expPos_preservestheoremProved here from basic factspropext, Classical.choice, Quot.sound

  /-- `exp : (ℝ, +) → (ℝ>0, ×)` preserves the operations; two elements of a subtype are equal
  when their values are (`Subtype.ext`), so this is `Real.exp_add` again. -/
  theorem expPos_preserves : PreservesOp expPos (· + ·) posMul :=
    fun x y => Subtype.ext (Real.exp_add x y)

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/StructurePreservingMaps.leanTry it in the Lean web editor

• log_exp_inversetheoremProved here from basic factspropext, Classical.choice, Quot.sound

  /-- `ln` and `exp` are inverse to each other between `ℝ` and `ℝ>0`:
  `ln (exp x) = x` (`Real.log_exp`) and `exp (ln u) = u` for `u > 0` (`Real.exp_log`). -/
  theorem log_exp_inverse :
      Function.LeftInverse logPos expPos ∧ Function.RightInverse logPos expPos :=
    ⟨fun x => Real.log_exp x, fun u => Subtype.ext (Real.exp_log u.2)⟩

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/StructurePreservingMaps.leanTry it in the Lean web editor

• logPos_preservestheoremProved here from basic factspropext, Classical.choice, Quot.sound

  /-- **`ln (uv) = ln u + ln v`, for free.** `exp` is a bijective homomorphism, so by
  `PreservesOp.inverse` its inverse `ln` is a homomorphism `(ℝ>0, ×) → (ℝ, +)`. We never touch
  the definition of the logarithm. -/
  theorem logPos_preserves : PreservesOp logPos posMul (· + ·) :=
    expPos_preserves.inverse log_exp_inverse.1 log_exp_inverse.2

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/StructurePreservingMaps.leanTry it in the Lean web editor

• no_injective_hom_zmod4_kleintheoremProved here from basic factspropext, Classical.choice, Quot.sound

  /-- **Clock arithmetic mod 4 is not isomorphic to the Klein four-group** `ℤ/2 × ℤ/2` — not even
  by an injective homomorphism. In `ℤ/2 × ℤ/2` every element satisfies `x + x = 0`. If `f`
  preserved addition, then `f (1 + 1) = f 1 + f 1 = 0 = f 0 + f 0 = f (0 + 0)`, and injectivity
  would give `1 + 1 = 0` in `ℤ/4`, which is false. -/
  theorem no_injective_hom_zmod4_klein :
      ¬ ∃ f : ZMod 4 → ZMod 2 × ZMod 2, Function.Injective f ∧ PreservesOp f (· + ·) (· + ·) := by
    rintro ⟨f, hinj, hf⟩
    have hdouble : ∀ x : ZMod 2 × ZMod 2, x + x = 0 := by decide
    have h : f (1 + 1) = f (0 + 0) :=
      calc f (1 + 1) = f 1 + f 1 := hf 1 1
        _ = 0 := hdouble _
        _ = f 0 + f 0 := (hdouble _).symm
        _ = f (0 + 0) := (hf 0 0).symm
    exact absurd (hinj h) (by decide)

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/StructurePreservingMaps.leanTry it in the Lean web editor

• zmod4_not_iso_kleintheoremProved here from basic factspropext, Classical.choice, Quot.sound

  /-- The same fact for Mathlib's bundled isomorphisms of additive groups (`≃+`): there is no
  `e : ZMod 4 ≃+ ZMod 2 × ZMod 2`, because `e` would be an injective homomorphism. -/
  theorem zmod4_not_iso_klein (e : ZMod 4 ≃+ ZMod 2 × ZMod 2) : False :=
    no_injective_hom_zmod4_klein ⟨e, e.injective, fun x y => map_add e x y⟩

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/StructurePreservingMaps.leanTry it in the Lean web editor

• crt6defDefinitionpropext, Quot.sound

  /-- The map `ℤ/6 → ℤ/2 × ℤ/3`, `x ↦ (x mod 2, x mod 3)`. (`ZMod.cast` reduces a residue
  mod 6 to a residue mod 2 or mod 3; this is well defined because 2 and 3 divide 6.) -/
  def crt6 (x : ZMod 6) : ZMod 2 × ZMod 3 :=
    (ZMod.cast x, ZMod.cast x)

  Axioms used: propext, Quot.soundformal/Lumenary/StructurePreservingMaps.leanTry it in the Lean web editor

• crt6_isotheoremProved here from basic factspropext, Classical.choice, Quot.sound

  /-- **`ℤ/6 ≅ ℤ/2 × ℤ/3`**: `crt6` is a bijection and preserves addition and multiplication.
  All three facts are finite checks over the 6 (or 36) cases, done by `decide`. -/
  theorem crt6_iso :
      Function.Bijective crt6 ∧ PreservesOp crt6 (· + ·) (· + ·) ∧
        PreservesOp crt6 (· * ·) (· * ·) := by
    unfold PreservesOp
    decide

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/StructurePreservingMaps.leanTry it in the Lean web editor

• crt6LibrarydefApplies a library theorempropext, Classical.choice, Quot.sound

  /-- Mathlib's version: the **Chinese remainder theorem** `ZMod.chineseRemainder` gives a ring
  isomorphism `ℤ/(mn) ≃+* ℤ/m × ℤ/n` whenever `m` and `n` are coprime. -/
  def crt6Library : ZMod 6 ≃+* ZMod 2 × ZMod 3 :=
    ZMod.chineseRemainder (by decide : Nat.Coprime 2 3)

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/StructurePreservingMaps.leanTry it in the Lean web editor

• PreservesReldefDefinitionNo axioms

  /-- For a **relation** (an order, the edges of a graph…), "preserving" means: related inputs have
  related outputs, `r x y → s (f x) (f y)`. -/
  def PreservesRel {A : Type u} {B : Type v} (f : A → B) (r : A → A → Prop) (s : B → B → Prop) :
      Prop :=
    ∀ x y, r x y → s (f x) (f y)

  Axioms used: No axiomsformal/Lumenary/StructurePreservingMaps.leanTry it in the Lean web editor

• bijection_not_isotheoremProved here from basic factspropext

  /-- **A structure-preserving bijection whose inverse does not preserve structure.** On `Bool`,
  compare the "discrete" order in which only `x ≤ x` holds (the relation `=`) with the usual order
  `false ≤ true`. The identity map is a bijection and preserves order from the discrete order to
  the usual one; but its inverse (the identity again, read backwards) sends `false ≤ true` to
  `false = true`, which fails. So for relations, "bijective and preserving" does not imply
  "isomorphism". -/
  theorem bijection_not_iso :
      Function.Bijective (id : Bool → Bool) ∧ PreservesRel (id : Bool → Bool) (· = ·) (· ≤ ·) ∧
        ¬ PreservesRel (id : Bool → Bool) (· ≤ ·) (· = ·) := by
    refine ⟨Function.bijective_id, ?_, ?_⟩
    · intro x y h
      subst h
      exact le_refl x
    · intro h
      have hft : false = true := h false true (by decide)
      exact Bool.false_ne_true hft

  Axioms used: propextformal/Lumenary/StructurePreservingMaps.leanTry it in the Lean web editor

• coloring_is_homtheoremApplies a library theorempropext, Classical.choice, Quot.sound

  /-- In Mathlib, a **colouring** of a graph `G` with colours `α` is *defined* to be a graph
  homomorphism from `G` to the complete graph on `α` (adjacent vertices must go to adjacent, that
  is, different, colours). This holds by Mathlib's definition `SimpleGraph.Coloring`. -/
  theorem coloring_is_hom {V : Type u} (G : SimpleGraph V) (α : Type v) :
      G.Coloring α = (G →g SimpleGraph.completeGraph α) :=
    rfl

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/StructurePreservingMaps.leanTry it in the Lean web editor

Formal exercises

Each exercise contains a sorry for you to replace. Open it in the Lean web editor, or clone the repository and run lake build.

/-- Composites of homomorphisms are homomorphisms.
Hint: `intro x y`, then a `calc` block with three steps: unfold `(g ∘ f) (opA x y)` to
`g (f (opA x y))` (`rfl`), rewrite with `hf`, finish with `hg`. -/
theorem PreservesOp.comp {A : Type u} {B : Type v} {C : Type w}
    {opA : A → A → A} {opB : B → B → B} {opC : C → C → C} {f : A → B} {g : B → C}
    (hf : PreservesOp f opA opB) (hg : PreservesOp g opB opC) :
    PreservesOp (g ∘ f) opA opC := by
  sorry

/-- **Composites of homomorphisms are homomorphisms.** If `f` turns `∗` into `⋆` and `g` turns
`⋆` into `•`, then `g ∘ f` turns `∗` into `•`:
`g(f(x ∗ y)) = g(f x ⋆ f y) = g(f x) • g(f y)`. -/
theorem PreservesOp.comp {A : Type u} {B : Type v} {C : Type w}
    {opA : A → A → A} {opB : B → B → B} {opC : C → C → C} {f : A → B} {g : B → C}
    (hf : PreservesOp f opA opB) (hg : PreservesOp g opB opC) :
    PreservesOp (g ∘ f) opA opC := by
  intro x y
  calc (g ∘ f) (opA x y) = g (f (opA x y)) := rfl
    _ = g (opB (f x) (f y)) := by rw [hf]
    _ = opC (g (f x)) (g (f y)) := hg _ _

/-- A surjective homomorphism carries commutativity across.
Hint: `obtain ⟨x, rfl⟩ := hsurj u` writes `u` as `f x`; do the same for `v`, then
`rw [← hf, ← hf, hcomm]`. -/
theorem comm_of_surjective {A : Type u} {B : Type v} {opA : A → A → A} {opB : B → B → B}
    {f : A → B} (hf : PreservesOp f opA opB) (hsurj : Function.Surjective f)
    (hcomm : ∀ x y, opA x y = opA y x) : ∀ u v, opB u v = opB v u := by
  sorry

/-- **Structure transfers along homomorphisms.** If `f` preserves the operation and is
surjective, and `∗` is commutative, then so is `⋆`: write `u = f x`, `v = f y`; then
`u ⋆ v = f (x ∗ y) = f (y ∗ x) = v ⋆ u`. In particular isomorphic structures are either both
commutative or both not. -/
theorem comm_of_surjective {A : Type u} {B : Type v} {opA : A → A → A} {opB : B → B → B}
    {f : A → B} (hf : PreservesOp f opA opB) (hsurj : Function.Surjective f)
    (hcomm : ∀ x y, opA x y = opA y x) : ∀ u v, opB u v = opB v u := by
  intro u v
  obtain ⟨x, rfl⟩ := hsurj u
  obtain ⟨y, rfl⟩ := hsurj v
  rw [← hf, ← hf, hcomm]