CompatibleInverseLimit.lean

def compatibleRingFamilies
    {ι : Type*} [Preorder ι] (R : ι → Type*) [∀ i, Ring (R i)]
    (transition : ∀ {i j : ι}, i ≤ j → R j →+* R i) :
    Subring (∀ i, R i) where
  carrier :=
    {x | ∀ {i j : ι} (hij : i ≤ j), transition hij (x j) = x i}
  zero_mem' := by
    intro i j hij
    exact map_zero (transition hij)
  one_mem' := by
    intro i j hij
    exact map_one (transition hij)
  add_mem' hx hy := by
    intro i j hij
    simpa using congrArg₂ (· + ·) (hx hij) (hy hij)
  mul_mem' hx hy := by
    intro i j hij
    simpa using congrArg₂ (· * ·) (hx hij) (hy hij)
  neg_mem' hx := by
    intro i j hij
    simpa using congrArg Neg.neg (hx hij)

def compatibleGroupFamilies
    {ι : Type*} [Preorder ι] (G : ι → Type*) [∀ i, Group (G i)]
    (transition : ∀ {i j : ι}, i ≤ j → G j →* G i) :
    Subgroup (∀ i, G i) where
  carrier :=
    {x | ∀ {i j : ι} (hij : i ≤ j), transition hij (x j) = x i}
  one_mem' := by
    intro i j hij
    exact map_one (transition hij)
  mul_mem' hx hy := by
    intro i j hij
    simpa using congrArg₂ (· * ·) (hx hij) (hy hij)
  inv_mem' hx := by
    intro i j hij
    simpa using congrArg Inv.inv (hx hij)

instance compatibleGroupFamiliesGroup
    {ι : Type*} [Preorder ι] (G : ι → Type*) [∀ i, Group (G i)]
    (transition : ∀ {i j : ι}, i ≤ j → G j →* G i) :
    Group (compatibleGroupFamilies G transition)

instance compatibleGroupFamiliesCommGroup
    {ι : Type*} [Preorder ι] (G : ι → Type*) [∀ i, CommGroup (G i)]
    (transition : ∀ {i j : ι}, i ≤ j → G j →* G i) :
    CommGroup (compatibleGroupFamilies G transition)

def compatibleGroupFamiliesEval
    {ι : Type*} [Preorder ι] (G : ι → Type*) [∀ i, Group (G i)]
    (transition : ∀ {i j : ι}, i ≤ j → G j →* G i) (i : ι) :
    compatibleGroupFamilies G transition →* G i

theorem compatibleGroupFamiliesEval_apply
    {ι : Type*} [Preorder ι] (G : ι → Type*) [∀ i, Group (G i)]
    (transition : ∀ {i j : ι}, i ≤ j → G j →* G i)
    (i : ι) (x : compatibleGroupFamilies G transition) :
    compatibleGroupFamiliesEval G transition i x = x.1 i

theorem compatibleGroupFamilies_transition
    {ι : Type*} [Preorder ι] (G : ι → Type*) [∀ i, Group (G i)]
    (transition : ∀ {i j : ι}, i ≤ j → G j →* G i)
    (x : compatibleGroupFamilies G transition) {i j : ι} (hij : i ≤ j) :
    transition hij (compatibleGroupFamiliesEval G transition j x) =
      compatibleGroupFamiliesEval G transition i x

theorem compatibleGroupFamilies_ext
    {ι : Type*} [Preorder ι] (G : ι → Type*) [∀ i, Group (G i)]
    (transition : ∀ {i j : ι}, i ≤ j → G j →* G i)
    {x y : compatibleGroupFamilies G transition}
    (h : ∀ i, compatibleGroupFamiliesEval G transition i x =
      compatibleGroupFamiliesEval G transition i y) : x = y

def compatibleGroupFamiliesMulEquiv
    {ι : Type*} [Preorder ι]
    (G H : ι → Type*) [∀ i, Group (G i)] [∀ i, Group (H i)]
    (transitionG : ∀ {i j : ι}, i ≤ j → G j →* G i)
    (transitionH : ∀ {i j : ι}, i ≤ j → H j →* H i)
    (e : ∀ i, G i ≃* H i)
    (hcomm : ∀ {i j : ι} (hij : i ≤ j) (x : G j),
      transitionH hij (e j x) = e i (transitionG hij x)) :
    compatibleGroupFamilies G transitionG ≃*
      compatibleGroupFamilies H transitionH where
  toFun x :=
    ⟨fun i => e i (x.1 i), by
      intro i j hij
      rw [hcomm hij, x.2 hij]⟩
  invFun y :=
    ⟨fun i => (e i).symm (y.1 i), by
      intro i j hij
      apply (e i).injective
      calc
        e i (transitionG hij ((e j).symm (y.1 j))) =
            transitionH hij (e j ((e j).symm (y.1 j))) :=
          (hcomm hij ((e j).symm (y.1 j))).symm
        _ = transitionH hij (y.1 j) := by rw [(e j).apply_symm_apply]
        _ = y.1 i := y.2 hij
        _ = e i ((e i).symm (y.1 i)) := by rw [(e i).apply_symm_apply]
      ⟩
  left_inv x := by
    ext i
    exact (e i).symm_apply_apply (x.1 i)
  right_inv y := by
    ext i
    exact (e i).apply_symm_apply (y.1 i)
  map_mul' x y := by
    ext i
    exact (e i).map_mul (x.1 i) (y.1 i)