Transitive classes for 3ʳᵈ iso thm

Stream: maths

[Visa]

Hi, I post here outcomes of my attempts to formalize the third isomorphism theorem (see Problems-with-3rd-iso-thm.lean). The idea was to encode substructure relation as a type class constraint. This raised multiple elaboration issues which could be useful to take into account in Lean 4. Especially inferring transitive classes could make this a compelling approach to use heavily in the algebra library. As such none of the attempts was really satisfactory.

[Rob Lewis]

For convenience, here's the file inline in a post:

import group_theory.coset ring_theory.matrix ring_theory.determinant ring_theory.ideals algebra.gcd_domain algebra.euclidean_domain data.int.modeq group_theory.quotient_group data.equiv.algebra group_theory.subgroup tactic.ring tactic.fin_cases tactic.tidy data.lazy_list category.monad.cont data.real.basic
open function quotient_group group is_group_hom set classical tactic

--- Notes on attempts to formalize the 3ʳᵈ group isomorphism theorem (K/G) / (H/G) ≅ K / H ---
---------------------------------------------------------------------------------------------
--The purpose of this document is to 1) present an encoding of subgroup relation as type class, 2) demonstrate type class inference problems and workarounds (especially inferring transitive classes—if possible in Lean 4—will solve the root problem), and 3) point out an auto_param bug.

variables{G H K : Type}[group G][group H][group K]
--The setup for the third isomorphism theorem for groups is that G ≤ H ⊴ K and G ⊴ K, which then imply G ⊴ H and H/G ⊴ K/G so that all the involved quotients are defined. The main problem in formalizing this is to have H/G become a subgroup of K/G. At the time of writing subgroup is defined to be a relation between a set and a type:
#check (@is_subgroup G _ : set G → Prop)
#check (@normal_subgroup G _ : set G → Prop)

--Within the context of Coq this problem was solved by "simulating set theory". Essentially one works with subsets of a type 𝔾 with axiomless group operations. Groups that have the same 𝔾 are subgroups of each other iff they are subsets of each other. This readily enables hierarchy like G≤H≤K. Groups with different 𝔾 can still not be compared, but it turns out that in practice 𝔾 usually ends up the same when needed. For example quotient H/G of 𝔾-groups H,G has different operational structure, but the new structure 𝔾/G only depends on G, and hence H/G and K/G are comparable. Even though this approach worked well for the odd order theorem, it has many drawbacks:
--additional 𝔾 layer complicates casual use
--backward incompatible with mathlib
--ℤ ≤ ℚ ≤ ℝ ≤ ℂ fails (or requires defining ℤ, ℚ and ℝ as subsets of ℂ)
--how does this fit to the algebraic hierarchy???
--not all natural group theoretic relations are captured, e.g. G ≰ G⋊H

meta def xx := tidy --can't be inlined

--Lean's implicit coercions make it feasible to mix elements from different types. Exploiting this I experimented representing subgroup relations by type classes.
class embed(G H : Type)[group G][group H] :=
(fn: G → H)
(inj: injective fn. xx)
(hom: is_group_hom fn. xx)
infixr `↪`:22 := embed

namespace embed
--Embedding can be interpreted as homomorphism and coercion.
instance: has_coe_to_fun(G↪H) := {F:=λ_,G→H, coe:= λi, i.fn}
instance[i: G↪H]: has_coe G H := ⟨i⟩
instance[i: G↪H]: is_group_hom i := i.hom
instance[i: G↪H]: is_subgroup(range i) := by apply_instance

--Existing formalization of subgroups can be reused.
@[reducible] def quot_by_embed(H G : Type)[group G][group H][i: G↪H] := quotient_group.quotient(range i)
infix ` ∕ `:70 := quot_by_embed

--Subgroup relations can be added retroactively by will.
/-
instance ℤℚ: multiplicative ℤ ↪ multiplicative ℚ := sorry
instance ℚℝ: multiplicative ℚ ↪ multiplicative ℝ := sorry
instance set{S: set G}[is_subgroup S]: S ↪ G := {fn:=subtype.val}

--PROBLEM 1: ↪ has to be transitive. Direct instance loops the type class inference:
instance[i: G↪H][j: H↪K]: G↪K := sorry
#check multiplicative ℝ ∕ multiplicative ℤ
--/
--Coercions overcome the problem of transitivity by using two classes: single-step and transitive one. With embeddings this is not ideal (messy details are exposed to users), but works.
class embed1(G H : Type)[group G][group H] :=
(fn: G → H)
(inj: injective fn. xx)
(hom: is_group_hom fn. xx)

instance trans[i: embed1 G H][j: H↪K]: G↪K := {
    fn:= j ∘ i.fn,
    inj:=by{have:=i.inj, have:=j.inj, xx},
    hom:=@is_group_hom.comp _ _ _ _ _ i.hom _ _ _ j.hom}
instance single[i: embed1 G H]: G↪H := {..i}

--Other instances are to be declared as single step ones.
instance ℤℚ: embed1 (multiplicative ℤ) (multiplicative ℚ) := sorry
instance ℚℝ: embed1 (multiplicative ℚ) (multiplicative ℝ) := sorry
instance set{S: set G}[is_subgroup S]: embed1 S G := {fn:=subtype.val}

--Now the basic example works, though because of general inefficiency in type class inference/hierarchy, a shortcut instance is needed.
instance groupℚ: group(multiplicative ℚ) := by apply_instance
#check multiplicative ℝ ∕ multiplicative ℤ


--Next the normality is added to the embeddings. Note that embed_normal is not an extension of embed_group but instead a property for it. This way it should be applicable to compositions of embeddings more flexibly.
class embed_normal(G H : Type)[group G][group H][i: G↪H] := {normal: normal_subgroup(range i)}
infix ` ⊴ `:50 := embed_normal

--Basic instances.
instance[i: G↪H][n: G⊴H]: normal_subgroup(range i) := n.normal
instance[i: G↪H][G⊴H]: group(H∕G) := by apply_instance

--PROBLEM 2: Unlike coercions embeddings appear as assumptions. When they do, one should use the transitive closure version ↪ to maximize usability, as is done so far. But assumptions also need to be transitively joined!
--instance[i: G↪H][j: H↪K][G⊴K/-Uuh!-/]: G⊴H := sorry

--A solution is to use auxiliarity definitions that only assume single step embeddings and then convert these into more flexible ones with a function like
def atomic_trans{R: embed1 G H → Sort*}(F: ∀[i₁: embed1 G H], R i₁)[i: G↪H] := @F{..i}

private def instance_normal_in_sub[i: embed1 G H][j: H↪K][G⊴K]: G⊴H := sorry
instance normal_in_sub := @atomic_trans G H _ _ _ (@instance_normal_in_sub G H K _ _ _)

private def instance_embed_quot[i: embed1 G H][j: H↪K][G⊴K][H⊴K]: H∕G ↪ K∕G := sorry
instance embed_quot := @atomic_trans G H _ _ _ (@instance_embed_quot G H K _ _ _)

private def instance_quot_normal[i: embed1 G H][j: H↪K][G⊴K][H⊴K]: H∕G ⊴ K∕G := sorry
instance quot_normal := @atomic_trans G H _ _ _ (@instance_quot_normal G H K _ _ _)

#check @embed.quot_normal G H K _ _ _ -- Π [i : G↪H] [j : H↪K] [_inst_4 : G ⊴ K] [_inst_5 : H ⊴ K], H ∕ G ⊴ K ∕ G


--Define the isomorphicity of groups.
structure group_equiv(G H : Type)[group G][group H] extends G ≃ H :=
    (hom: is_group_hom to_fun)
    (inv_hom: is_group_hom inv_fun)
infix ` ≅ `:50 := group_equiv


--PROBLEM 3: This results in an undebuggable mess—the failing instance trace doesn't even show up (for me)!
--set_option trace.class_instances true
private def isomorphism_theorem_3'[i: embed1 G H][j: H↪K][G⊴K][H⊴K]: (K∕G) ∕ (H∕G) ≅ K ∕ H := sorry

--I was able to formalize a version of the third isomorphism theorem using this approach and packed groups.
structure Group := (base: Type*) (struct: group base)
--This is however incompatible with mathlib, complicates casual use, and possibly reproduces the inference problems once number of defined class instances increases.
end embed
--------------------------------------------------------------------------------------------


--Another way to overcome problem 1 is to apply custom transitivity-aware inference via auto_params. Quotient ∕ and normality ⊴ are changed so that instead of type class search [i: G↪H] they use custom search (i: G↪H. custom_trans_inf_tactic). In addition to just sequencing embeddings transitively such custom search must do general type class inference (already here embed_quot must be used to type quot_normal). Currently type class inference can't be hooked (auto_params remain passive during inference, but just activating them wouldn't give required control). Hence the custom search had to reimplement type class search in Lean. This way neither single-step class nor atomic_trans are needed, and the third isomorphism theorem can be formalized as:
--theorem isomorphism_theorem_3{i: G↪H}{j: H↪K}[nj: H⊴K][nji: G⊴K]:
--  let hg:=H∕G, kg:=K∕G in kg∕hg ≅ K∕H --The let...in is necessary!
--:= ...
--PROBLEM 4: The goal auto_param should fullfill is not always revealed. Instead it shows up as unassigned meta variable. This happens when inferences are nested or multiple parameters need to be inferred. The problem occures only with result types, not with parameter types. Nesting can be worked around using lets, which is what happens in the isomorphism_theorem_3 above. Minimal examples follow.
meta def a := target >>= trace >> assumption --Print the goal and guess solution.
def A(x:Type)(_:x. a)(_:x. a) := x
def B(x:Type)(i:x): A x := i --A doesn't see its first goal.
def C(x:Type)(_:x. a) := x
def D(x:Type)(_:x. a) := x
def E(x:Type)(i:x): D(C x) := i --D doesn't see that goal is C x.
--This problem likely exists for a reason: how could the system decide which auto_param to solve first? As with hooking the type class search, this ideally asks an intelligent default or fine grained control over, how auto_params interact with elaboration and each others. In any case the current behavior obviously ignores available data.

--Full code is available at https://github.com/0function/storage in files group_isomorphicity.lean and transitive_class_inference.lean.