Skip to content

Instantly share code, notes, and snippets.

@Timeroot
Created October 13, 2021 06:03
Show Gist options
  • Save Timeroot/65e4e8a5b7a4216251f425c0e1cd1da1 to your computer and use it in GitHub Desktop.
Save Timeroot/65e4e8a5b7a4216251f425c0e1cd1da1 to your computer and use it in GitHub Desktop.
Minimal example for struggling to show that some object mappings are inverses.
import algebra.group_with_zero
import data.equiv.mul_add
universe u
variables {S : Type*}
--We're going to show the 1-to-1 correspondence between groups (with additive notation)
--and groups_with_zero (with multiplicative notation). To make the mapping less trivial,
--we'll also use the opposite group: so a+b becomes b*a.
--First define how we multiply (with zero) from elements in an additive group.
--The operation:
def g₀_add_op [add_group S]: option S → option S → option S
| none _ := none
| _ none := none
| (some a) (some b) := some (b+a)
--The actual map:
def convert_g_into_g₀_op (g : add_group S) : group_with_zero (option S) := {
mul := g₀_add_op,
inv := begin intro a, cases a, exact none, exact some (-a) end,
zero := none,
one := some 0,
mul_assoc := begin intros, cases a; cases b; cases c; simp [g₀_add_op], exact (add_assoc c b a).symm end,
one_mul := begin intro, cases a; simp [g₀_add_op] end,
mul_one := begin intro, cases a; simp [g₀_add_op] end,
zero_mul := begin intro, cases a; simp [g₀_add_op] end,
mul_zero := begin intro, cases a; simp [g₀_add_op] end,
exists_pair_ne := ⟨none, some 0, by simp⟩,
inv_zero := sorry, mul_inv_cancel := sorry
}
--Then the map from a group with zero back to an additive group defined on the units:
def convert_g₀_into_g_op (g0 : group_with_zero S) : add_group (units S) := {
add := λ a b, b*a,
neg := λ a, a⁻¹,
zero := 1,
add_assoc := begin intros, simp, exact (mul_assoc c b a).symm end,
zero_add := by simp,
add_zero := by simp,
add_left_neg := sorry
}
--The syntax below is what's wrong and where I'm stuck.
--I want to show that convert_g_into_g₀_op and convert_g₀_into_g_op are inverses,
--in the sense that
-- convert_g_into_g₀_op (convert_g₀_into_g_op G) ≃* G
--for any group_with_zero G, and that
-- convert_g₀_into_g_op (convert_g_into_g₀_op G) ≃+ G
--for any add_group G.
def group_gzero_iso [g : add_group S]: convert_g₀_into_g_op (convert_g_into_g₀_op g) ≃+ g :=
begin
sorry
end
def gzero_group_iso [g0 : group_with_zero S]: convert_g_into_g₀_op (convert_g₀_into_g_op g0) ≃* g0 :=
begin
sorry
end
@Timeroot
Copy link
Author

I have found the correct type signature for group_gzero_iso. Unfortunately, as written, it is awful.

def group_gzero_iso [g : add_group S]: @@add_equiv
  S
  (@@units (option S) 
    (@@monoid_with_zero.to_monoid
      (option S)
      (@@group_with_zero.to_monoid_with_zero (option S) (convert_g_into_g₀_op g)
  ) ) )
  (@@add_semigroup.to_has_add S (add_monoid.to_add_semigroup S))
  (@@add_semigroup.to_has_add
    (@@units (option S) 
      (@@monoid_with_zero.to_monoid
        (option S)
        (@@group_with_zero.to_monoid_with_zero (option S) (convert_g_into_g₀_op g)
    ) ) )
    (@@add_monoid.to_add_semigroup
      (@@units (option S) 
        (@@monoid_with_zero.to_monoid
          (option S)
          (@@group_with_zero.to_monoid_with_zero (option S) (convert_g_into_g₀_op g)
      ) ) )
      (@@add_group.to_add_monoid
        (@@units (option S) 
          (@@monoid_with_zero.to_monoid
            (option S)
            (@@group_with_zero.to_monoid_with_zero (option S) (convert_g_into_g₀_op g)
        ) ) )
        (convert_g₀_into_g_op (convert_g_into_g₀_op g))
  ) ) ) :=
begin
  sorry
end

@Timeroot
Copy link
Author

Found a good solution! Add

@[ancestor add_equiv]
structure add_equiv_with_structure {M N : Type*} {child : Type u → Type u}
  (cM : child M) (cN : child N) [hM : has_add M] [hN : has_add N]  extends M ≃+ N

@[ancestor mul_equiv, to_additive]
structure mul_equiv_with_structure {M N : Type*} {child : Type u → Type u}
  (cM : child M) (cN : child N) [hM : has_mul M] [hN : has_mul N] extends M ≃* N

infix ` ≃*' `:25 := mul_equiv_with_structure
infix ` ≃+' `:25 := add_equiv_with_structure

and then one can just write

def group_gzero_iso [g : add_group S]: convert_g₀_into_g_op (convert_g_into_g₀_op g) ≃+' g := sorry

with the extra apostrophe in ≃+'. The "child" lets it accept the group S, but then infer the has_mul S structure from that group, and turn that into a mul_equiv with no apostrophe.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment