text:
/-
Copyright (c) 2019 Scott Morrison. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Scott Morrison, Floris van Doorn

! This file was ported from Lean 3 source module category_theory.limits.opposites
! leanprover-community/mathlib commit 69c6a5a12d8a2b159f20933e60115a4f2de62b58
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathbin.CategoryTheory.Limits.Filtered
import Mathbin.CategoryTheory.Limits.Shapes.FiniteProducts
import Mathbin.CategoryTheory.DiscreteCategory
import Mathbin.Tactic.EquivRw

/-!
# Limits in `C` give colimits in `Cᵒᵖ`.

> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
> Any changes to this file require a corresponding PR to mathlib4.

We also give special cases for (co)products,
(co)equalizers, and pullbacks / pushouts.

-/

universe v₁ v₂ u₁ u₂

noncomputable section

open CategoryTheory

open CategoryTheory.Functor

open Opposite

namespace CategoryTheory.Limits

variable {C : Type u₁} [Category.{v₁} C]

variable {J : Type u₂} [Category.{v₂} J]

#print CategoryTheory.Limits.isLimitCoconeOp /-
/-- Turn a colimit for `F : J ⥤ C` into a limit for `F.op : Jᵒᵖ ⥤ Cᵒᵖ`. -/
@[simps]
def isLimitCoconeOp (F : J ⥤ C) {c : Cocone F} (hc : IsColimit c) : IsLimit c.op
    where
  lift s := (hc.desc s.unop).op
  fac s j := Quiver.Hom.unop_inj (by simpa)
  uniq s m w := by
    refine' Quiver.Hom.unop_inj (hc.hom_ext fun j => Quiver.Hom.op_inj _)
    simpa only [Quiver.Hom.unop_op, is_colimit.fac] using w (op j)
#align category_theory.limits.is_limit_cocone_op CategoryTheory.Limits.isLimitCoconeOp
-/

#print CategoryTheory.Limits.isColimitConeOp /-
/-- Turn a limit for `F : J ⥤ C` into a colimit for `F.op : Jᵒᵖ ⥤ Cᵒᵖ`. -/
@[simps]
def isColimitConeOp (F : J ⥤ C) {c : Cone F} (hc : IsLimit c) : IsColimit c.op
    where
  desc s := (hc.lift s.unop).op
  fac s j := Quiver.Hom.unop_inj (by simpa)
  uniq s m w := by
    refine' Quiver.Hom.unop_inj (hc.hom_ext fun j => Quiver.Hom.op_inj _)
    simpa only [Quiver.Hom.unop_op, is_limit.fac] using w (op j)
#align category_theory.limits.is_colimit_cone_op CategoryTheory.Limits.isColimitConeOp
-/

#print CategoryTheory.Limits.isLimitConeLeftOpOfCocone /-
/-- Turn a colimit for `F : J ⥤ Cᵒᵖ` into a limit for `F.left_op : Jᵒᵖ ⥤ C`. -/
@[simps]
def isLimitConeLeftOpOfCocone (F : J ⥤ Cᵒᵖ) {c : Cocone F} (hc : IsColimit c) :
    IsLimit (coneLeftOpOfCocone c)
    where
  lift s := (hc.desc (coconeOfConeLeftOp s)).unop
  fac s j :=
    Quiver.Hom.op_inj <| by
      simpa only [cone_left_op_of_cocone_π_app, op_comp, Quiver.Hom.op_unop, is_colimit.fac,
        cocone_of_cone_left_op_ι_app]
  uniq s m w := by
    refine' Quiver.Hom.op_inj (hc.hom_ext fun j => Quiver.Hom.unop_inj _)
    simpa only [Quiver.Hom.op_unop, is_colimit.fac, cocone_of_cone_left_op_ι_app] using w (op j)
#align category_theory.limits.is_limit_cone_left_op_of_cocone CategoryTheory.Limits.isLimitConeLeftOpOfCocone
-/

#print CategoryTheory.Limits.isColimitCoconeLeftOpOfCone /-
/-- Turn a limit of `F : J ⥤ Cᵒᵖ` into a colimit of `F.left_op : Jᵒᵖ ⥤ C`. -/
@[simps]
def isColimitCoconeLeftOpOfCone (F : J ⥤ Cᵒᵖ) {c : Cone F} (hc : IsLimit c) :
    IsColimit (coconeLeftOpOfCone c)
    where
  desc s := (hc.lift (coneOfCoconeLeftOp s)).unop
  fac s j :=
    Quiver.Hom.op_inj <| by
      simpa only [cocone_left_op_of_cone_ι_app, op_comp, Quiver.Hom.op_unop, is_limit.fac,
        cone_of_cocone_left_op_π_app]
  uniq s m w := by
    refine' Quiver.Hom.op_inj (hc.hom_ext fun j => Quiver.Hom.unop_inj _)
    simpa only [Quiver.Hom.op_unop, is_limit.fac, cone_of_cocone_left_op_π_app] using w (op j)
#align category_theory.limits.is_colimit_cocone_left_op_of_cone CategoryTheory.Limits.isColimitCoconeLeftOpOfCone
-/

#print CategoryTheory.Limits.isLimitConeRightOpOfCocone /-
/-- Turn a colimit for `F : Jᵒᵖ ⥤ C` into a limit for `F.right_op : J ⥤ Cᵒᵖ`. -/
@[simps]
def isLimitConeRightOpOfCocone (F : Jᵒᵖ ⥤ C) {c : Cocone F} (hc : IsColimit c) :
    IsLimit (coneRightOpOfCocone c)
    where
  lift s := (hc.desc (coconeOfConeRightOp s)).op
  fac s j := Quiver.Hom.unop_inj (by simpa)
  uniq s m w := by
    refine' Quiver.Hom.unop_inj (hc.hom_ext fun j => Quiver.Hom.op_inj _)
    simpa only [Quiver.Hom.unop_op, is_colimit.fac] using w (unop j)
#align category_theory.limits.is_limit_cone_right_op_of_cocone CategoryTheory.Limits.isLimitConeRightOpOfCocone
-/

#print CategoryTheory.Limits.isColimitCoconeRightOpOfCone /-
/-- Turn a limit for `F : Jᵒᵖ ⥤ C` into a colimit for `F.right_op : J ⥤ Cᵒᵖ`. -/
@[simps]
def isColimitCoconeRightOpOfCone (F : Jᵒᵖ ⥤ C) {c : Cone F} (hc : IsLimit c) :
    IsColimit (coconeRightOpOfCone c)
    where
  desc s := (hc.lift (coneOfCoconeRightOp s)).op
  fac s j := Quiver.Hom.unop_inj (by simpa)
  uniq s m w := by
    refine' Quiver.Hom.unop_inj (hc.hom_ext fun j => Quiver.Hom.op_inj _)
    simpa only [Quiver.Hom.unop_op, is_limit.fac] using w (unop j)
#align category_theory.limits.is_colimit_cocone_right_op_of_cone CategoryTheory.Limits.isColimitCoconeRightOpOfCone
-/

#print CategoryTheory.Limits.isLimitConeUnopOfCocone /-
/-- Turn a colimit for `F : Jᵒᵖ ⥤ Cᵒᵖ` into a limit for `F.unop : J ⥤ C`. -/
@[simps]
def isLimitConeUnopOfCocone (F : Jᵒᵖ ⥤ Cᵒᵖ) {c : Cocone F} (hc : IsColimit c) :
    IsLimit (coneUnopOfCocone c)
    where
  lift s := (hc.desc (coconeOfConeUnop s)).unop
  fac s j := Quiver.Hom.op_inj (by simpa)
  uniq s m w := by
    refine' Quiver.Hom.op_inj (hc.hom_ext fun j => Quiver.Hom.unop_inj _)
    simpa only [Quiver.Hom.op_unop, is_colimit.fac] using w (unop j)
#align category_theory.limits.is_limit_cone_unop_of_cocone CategoryTheory.Limits.isLimitConeUnopOfCocone
-/

#print CategoryTheory.Limits.isColimitCoconeUnopOfCone /-
/-- Turn a limit of `F : Jᵒᵖ ⥤ Cᵒᵖ` into a colimit of `F.unop : J ⥤ C`. -/
@[simps]
def isColimitCoconeUnopOfCone (F : Jᵒᵖ ⥤ Cᵒᵖ) {c : Cone F} (hc : IsLimit c) :
    IsColimit (coconeUnopOfCone c)
    where
  desc s := (hc.lift (coneOfCoconeUnop s)).unop
  fac s j := Quiver.Hom.op_inj (by simpa)
  uniq s m w := by
    refine' Quiver.Hom.op_inj (hc.hom_ext fun j => Quiver.Hom.unop_inj _)
    simpa only [Quiver.Hom.op_unop, is_limit.fac] using w (unop j)
#align category_theory.limits.is_colimit_cocone_unop_of_cone CategoryTheory.Limits.isColimitCoconeUnopOfCone
-/

#print CategoryTheory.Limits.isLimitCoconeUnop /-
/-- Turn a colimit for `F.op : Jᵒᵖ ⥤ Cᵒᵖ` into a limit for `F : J ⥤ C`. -/
@[simps]
def isLimitCoconeUnop (F : J ⥤ C) {c : Cocone F.op} (hc : IsColimit c) : IsLimit c.unop
    where
  lift s := (hc.desc s.op).unop
  fac s j := Quiver.Hom.op_inj (by simpa)
  uniq s m w := by
    refine' Quiver.Hom.op_inj (hc.hom_ext fun j => Quiver.Hom.unop_inj _)
    simpa only [Quiver.Hom.op_unop, is_colimit.fac] using w (unop j)
#align category_theory.limits.is_limit_cocone_unop CategoryTheory.Limits.isLimitCoconeUnop
-/

#print CategoryTheory.Limits.isColimitConeUnop /-
/-- Turn a limit for `F.op : Jᵒᵖ ⥤ Cᵒᵖ` into a colimit for `F : J ⥤ C`. -/
@[simps]
def isColimitConeUnop (F : J ⥤ C) {c : Cone F.op} (hc : IsLimit c) : IsColimit c.unop
    where
  desc s := (hc.lift s.op).unop
  fac s j := Quiver.Hom.op_inj (by simpa)
  uniq s m w := by
    refine' Quiver.Hom.op_inj (hc.hom_ext fun j => Quiver.Hom.unop_inj _)
    simpa only [Quiver.Hom.op_unop, is_limit.fac] using w (unop j)
#align category_theory.limits.is_colimit_cone_unop CategoryTheory.Limits.isColimitConeUnop
-/

#print CategoryTheory.Limits.isLimitConeOfCoconeLeftOp /-
/-- Turn a colimit for `F.left_op : Jᵒᵖ ⥤ C` into a limit for `F : J ⥤ Cᵒᵖ`. -/
@[simps]
def isLimitConeOfCoconeLeftOp (F : J ⥤ Cᵒᵖ) {c : Cocone F.leftOp} (hc : IsColimit c) :
    IsLimit (coneOfCoconeLeftOp c)
    where
  lift s := (hc.desc (coconeLeftOpOfCone s)).op
  fac s j :=
    Quiver.Hom.unop_inj <| by
      simpa only [cone_of_cocone_left_op_π_app, unop_comp, Quiver.Hom.unop_op, is_colimit.fac,
        cocone_left_op_of_cone_ι_app]
  uniq s m w := by
    refine' Quiver.Hom.unop_inj (hc.hom_ext fun j => Quiver.Hom.op_inj _)
    simpa only [Quiver.Hom.unop_op, is_colimit.fac, cone_of_cocone_left_op_π_app] using w (unop j)
#align category_theory.limits.is_limit_cone_of_cocone_left_op CategoryTheory.Limits.isLimitConeOfCoconeLeftOp
-/

#print CategoryTheory.Limits.isColimitCoconeOfConeLeftOp /-
/-- Turn a limit of `F.left_op : Jᵒᵖ ⥤ C` into a colimit of `F : J ⥤ Cᵒᵖ`. -/
@[simps]
def isColimitCoconeOfConeLeftOp (F : J ⥤ Cᵒᵖ) {c : Cone F.leftOp} (hc : IsLimit c) :
    IsColimit (coconeOfConeLeftOp c)
    where
  desc s := (hc.lift (coneLeftOpOfCocone s)).op
  fac s j :=
    Quiver.Hom.unop_inj <| by
      simpa only [cocone_of_cone_left_op_ι_app, unop_comp, Quiver.Hom.unop_op, is_limit.fac,
        cone_left_op_of_cocone_π_app]
  uniq s m w := by
    refine' Quiver.Hom.unop_inj (hc.hom_ext fun j => Quiver.Hom.op_inj _)
    simpa only [Quiver.Hom.unop_op, is_limit.fac, cocone_of_cone_left_op_ι_app] using w (unop j)
#align category_theory.limits.is_colimit_cocone_of_cone_left_op CategoryTheory.Limits.isColimitCoconeOfConeLeftOp
-/

#print CategoryTheory.Limits.isLimitConeOfCoconeRightOp /-
/-- Turn a colimit for `F.right_op : J ⥤ Cᵒᵖ` into a limit for `F : Jᵒᵖ ⥤ C`. -/
@[simps]
def isLimitConeOfCoconeRightOp (F : Jᵒᵖ ⥤ C) {c : Cocone F.rightOp} (hc : IsColimit c) :
    IsLimit (coneOfCoconeRightOp c)
    where
  lift s := (hc.desc (coconeRightOpOfCone s)).unop
  fac s j := Quiver.Hom.op_inj (by simpa)
  uniq s m w := by
    refine' Quiver.Hom.op_inj (hc.hom_ext fun j => Quiver.Hom.unop_inj _)
    simpa only [Quiver.Hom.op_unop, is_colimit.fac] using w (op j)
#align category_theory.limits.is_limit_cone_of_cocone_right_op CategoryTheory.Limits.isLimitConeOfCoconeRightOp
-/

#print CategoryTheory.Limits.isColimitCoconeOfConeRightOp /-
/-- Turn a limit for `F.right_op : J ⥤ Cᵒᵖ` into a limit for `F : Jᵒᵖ ⥤ C`. -/
@[simps]
def isColimitCoconeOfConeRightOp (F : Jᵒᵖ ⥤ C) {c : Cone F.rightOp} (hc : IsLimit c) :
    IsColimit (coconeOfConeRightOp c)
    where
  desc s := (hc.lift (coneRightOpOfCocone s)).unop
  fac s j := Quiver.Hom.op_inj (by simpa)
  uniq s m w := by
    refine' Quiver.Hom.op_inj (hc.hom_ext fun j => Quiver.Hom.unop_inj _)
    simpa only [Quiver.Hom.op_unop, is_limit.fac] using w (op j)
#align category_theory.limits.is_colimit_cocone_of_cone_right_op CategoryTheory.Limits.isColimitCoconeOfConeRightOp
-/

#print CategoryTheory.Limits.isLimitConeOfCoconeUnop /-
/-- Turn a colimit for `F.unop : J ⥤ C` into a limit for `F : Jᵒᵖ ⥤ Cᵒᵖ`. -/
@[simps]
def isLimitConeOfCoconeUnop (F : Jᵒᵖ ⥤ Cᵒᵖ) {c : Cocone F.unop} (hc : IsColimit c) :
    IsLimit (coneOfCoconeUnop c)
    where
  lift s := (hc.desc (coconeUnopOfCone s)).op
  fac s j := Quiver.Hom.unop_inj (by simpa)
  uniq s m w := by
    refine' Quiver.Hom.unop_inj (hc.hom_ext fun j => Quiver.Hom.op_inj _)
    simpa only [Quiver.Hom.unop_op, is_colimit.fac] using w (op j)
#align category_theory.limits.is_limit_cone_of_cocone_unop CategoryTheory.Limits.isLimitConeOfCoconeUnop
-/

#print CategoryTheory.Limits.isColimitConeOfCoconeUnop /-
/-- Turn a limit for `F.unop : J ⥤ C` into a colimit for `F : Jᵒᵖ ⥤ Cᵒᵖ`. -/
@[simps]
def isColimitConeOfCoconeUnop (F : Jᵒᵖ ⥤ Cᵒᵖ) {c : Cone F.unop} (hc : IsLimit c) :
    IsColimit (coconeOfConeUnop c)
    where
  desc s := (hc.lift (coneUnopOfCocone s)).op
  fac s j := Quiver.Hom.unop_inj (by simpa)
  uniq s m w := by
    refine' Quiver.Hom.unop_inj (hc.hom_ext fun j => Quiver.Hom.op_inj _)
    simpa only [Quiver.Hom.unop_op, is_limit.fac] using w (op j)
#align category_theory.limits.is_colimit_cone_of_cocone_unop CategoryTheory.Limits.isColimitConeOfCoconeUnop
-/

#print CategoryTheory.Limits.hasLimit_of_hasColimit_leftOp /-
/-- If `F.left_op : Jᵒᵖ ⥤ C` has a colimit, we can construct a limit for `F : J ⥤ Cᵒᵖ`.
-/
theorem hasLimit_of_hasColimit_leftOp (F : J ⥤ Cᵒᵖ) [HasColimit F.leftOp] : HasLimit F :=
  HasLimit.mk
    { Cone := coneOfCoconeLeftOp (colimit.cocone F.leftOp)
      IsLimit := isLimitConeOfCoconeLeftOp _ (colimit.isColimit _) }
#align category_theory.limits.has_limit_of_has_colimit_left_op CategoryTheory.Limits.hasLimit_of_hasColimit_leftOp
-/

#print CategoryTheory.Limits.hasLimit_of_hasColimit_op /-
theorem hasLimit_of_hasColimit_op (F : J ⥤ C) [HasColimit F.op] : HasLimit F :=
  HasLimit.mk
    { Cone := (colimit.cocone F.op).unop
      IsLimit := isLimitCoconeUnop _ (colimit.isColimit _) }
#align category_theory.limits.has_limit_of_has_colimit_op CategoryTheory.Limits.hasLimit_of_hasColimit_op
-/

#print CategoryTheory.Limits.hasLimitsOfShape_op_of_hasColimitsOfShape /-
/-- If `C` has colimits of shape `Jᵒᵖ`, we can construct limits in `Cᵒᵖ` of shape `J`.
-/
theorem hasLimitsOfShape_op_of_hasColimitsOfShape [HasColimitsOfShape Jᵒᵖ C] :
    HasLimitsOfShape J Cᵒᵖ :=
  { HasLimit := fun F => hasLimit_of_hasColimit_leftOp F }
#align category_theory.limits.has_limits_of_shape_op_of_has_colimits_of_shape CategoryTheory.Limits.hasLimitsOfShape_op_of_hasColimitsOfShape
-/

#print CategoryTheory.Limits.hasLimitsOfShape_of_hasColimitsOfShape_op /-
theorem hasLimitsOfShape_of_hasColimitsOfShape_op [HasColimitsOfShape Jᵒᵖ Cᵒᵖ] :
    HasLimitsOfShape J C :=
  { HasLimit := fun F => hasLimit_of_hasColimit_op F }
#align category_theory.limits.has_limits_of_shape_of_has_colimits_of_shape_op CategoryTheory.Limits.hasLimitsOfShape_of_hasColimitsOfShape_op
-/

attribute [local instance] has_limits_of_shape_op_of_has_colimits_of_shape

#print CategoryTheory.Limits.hasLimits_op_of_hasColimits /-
/-- If `C` has colimits, we can construct limits for `Cᵒᵖ`.
-/
instance hasLimits_op_of_hasColimits [HasColimits C] : HasLimits Cᵒᵖ :=
  ⟨inferInstance⟩
#align category_theory.limits.has_limits_op_of_has_colimits CategoryTheory.Limits.hasLimits_op_of_hasColimits
-/

#print CategoryTheory.Limits.hasLimits_of_hasColimits_op /-
theorem hasLimits_of_hasColimits_op [HasColimits Cᵒᵖ] : HasLimits C :=
  { HasLimitsOfShape := fun J hJ => has_limits_of_shape_of_has_colimits_of_shape_op }
#align category_theory.limits.has_limits_of_has_colimits_op CategoryTheory.Limits.hasLimits_of_hasColimits_op
-/

#print CategoryTheory.Limits.has_cofiltered_limits_op_of_has_filtered_colimits /-
instance has_cofiltered_limits_op_of_has_filtered_colimits [HasFilteredColimitsOfSize.{v₂, u₂} C] :
    HasCofilteredLimitsOfSize.{v₂, u₂} Cᵒᵖ
    where HasLimitsOfShape I hI₁ hI₂ := has_limits_of_shape_op_of_has_colimits_of_shape
#align category_theory.limits.has_cofiltered_limits_op_of_has_filtered_colimits CategoryTheory.Limits.has_cofiltered_limits_op_of_has_filtered_colimits
-/

#print CategoryTheory.Limits.has_cofiltered_limits_of_has_filtered_colimits_op /-
theorem has_cofiltered_limits_of_has_filtered_colimits_op [HasFilteredColimitsOfSize.{v₂, u₂} Cᵒᵖ] :
    HasCofilteredLimitsOfSize.{v₂, u₂} C :=
  { HasLimitsOfShape := fun I hI₂ hI₂ => has_limits_of_shape_of_has_colimits_of_shape_op }
#align category_theory.limits.has_cofiltered_limits_of_has_filtered_colimits_op CategoryTheory.Limits.has_cofiltered_limits_of_has_filtered_colimits_op
-/

#print CategoryTheory.Limits.hasColimit_of_hasLimit_leftOp /-
/-- If `F.left_op : Jᵒᵖ ⥤ C` has a limit, we can construct a colimit for `F : J ⥤ Cᵒᵖ`.
-/
theorem hasColimit_of_hasLimit_leftOp (F : J ⥤ Cᵒᵖ) [HasLimit F.leftOp] : HasColimit F :=
  HasColimit.mk
    { Cocone := coconeOfConeLeftOp (limit.cone F.leftOp)
      IsColimit := isColimitCoconeOfConeLeftOp _ (limit.isLimit _) }
#align category_theory.limits.has_colimit_of_has_limit_left_op CategoryTheory.Limits.hasColimit_of_hasLimit_leftOp
-/

#print CategoryTheory.Limits.hasColimit_of_hasLimit_op /-
theorem hasColimit_of_hasLimit_op (F : J ⥤ C) [HasLimit F.op] : HasColimit F :=
  HasColimit.mk
    { Cocone := (limit.cone F.op).unop
      IsColimit := isColimitConeUnop _ (limit.isLimit _) }
#align category_theory.limits.has_colimit_of_has_limit_op CategoryTheory.Limits.hasColimit_of_hasLimit_op
-/

#print CategoryTheory.Limits.hasColimitsOfShape_op_of_hasLimitsOfShape /-
/-- If `C` has colimits of shape `Jᵒᵖ`, we can construct limits in `Cᵒᵖ` of shape `J`.
-/
instance hasColimitsOfShape_op_of_hasLimitsOfShape [HasLimitsOfShape Jᵒᵖ C] :
    HasColimitsOfShape J Cᵒᵖ where HasColimit F := hasColimit_of_hasLimit_leftOp F
#align category_theory.limits.has_colimits_of_shape_op_of_has_limits_of_shape CategoryTheory.Limits.hasColimitsOfShape_op_of_hasLimitsOfShape
-/

#print CategoryTheory.Limits.hasColimitsOfShape_of_hasLimitsOfShape_op /-
theorem hasColimitsOfShape_of_hasLimitsOfShape_op [HasLimitsOfShape Jᵒᵖ Cᵒᵖ] :
    HasColimitsOfShape J C :=
  { HasColimit := fun F => hasColimit_of_hasLimit_op F }
#align category_theory.limits.has_colimits_of_shape_of_has_limits_of_shape_op CategoryTheory.Limits.hasColimitsOfShape_of_hasLimitsOfShape_op
-/

#print CategoryTheory.Limits.hasColimits_op_of_hasLimits /-
/-- If `C` has limits, we can construct colimits for `Cᵒᵖ`.
-/
instance hasColimits_op_of_hasLimits [HasLimits C] : HasColimits Cᵒᵖ :=
  ⟨inferInstance⟩
#align category_theory.limits.has_colimits_op_of_has_limits CategoryTheory.Limits.hasColimits_op_of_hasLimits
-/

#print CategoryTheory.Limits.hasColimits_of_hasLimits_op /-
theorem hasColimits_of_hasLimits_op [HasLimits Cᵒᵖ] : HasColimits C :=
  { HasColimitsOfShape := fun J hJ => has_colimits_of_shape_of_has_limits_of_shape_op }
#align category_theory.limits.has_colimits_of_has_limits_op CategoryTheory.Limits.hasColimits_of_hasLimits_op
-/

#print CategoryTheory.Limits.has_filtered_colimits_op_of_has_cofiltered_limits /-
instance has_filtered_colimits_op_of_has_cofiltered_limits [HasCofilteredLimitsOfSize.{v₂, u₂} C] :
    HasFilteredColimitsOfSize.{v₂, u₂} Cᵒᵖ where HasColimitsOfShape I hI₁ hI₂ := inferInstance
#align category_theory.limits.has_filtered_colimits_op_of_has_cofiltered_limits CategoryTheory.Limits.has_filtered_colimits_op_of_has_cofiltered_limits
-/

#print CategoryTheory.Limits.has_filtered_colimits_of_has_cofiltered_limits_op /-
theorem has_filtered_colimits_of_has_cofiltered_limits_op [HasCofilteredLimitsOfSize.{v₂, u₂} Cᵒᵖ] :
    HasFilteredColimitsOfSize.{v₂, u₂} C :=
  { HasColimitsOfShape := fun I hI₁ hI₂ => has_colimits_of_shape_of_has_limits_of_shape_op }
#align category_theory.limits.has_filtered_colimits_of_has_cofiltered_limits_op CategoryTheory.Limits.has_filtered_colimits_of_has_cofiltered_limits_op
-/

variable (X : Type v₂)

#print CategoryTheory.Limits.hasCoproductsOfShape_opposite /-
/-- If `C` has products indexed by `X`, then `Cᵒᵖ` has coproducts indexed by `X`.
-/
instance hasCoproductsOfShape_opposite [HasProductsOfShape X C] : HasCoproductsOfShape X Cᵒᵖ :=
  by
  haveI : has_limits_of_shape (discrete X)ᵒᵖ C :=
    has_limits_of_shape_of_equivalence (discrete.opposite X).symm
  infer_instance
#align category_theory.limits.has_coproducts_of_shape_opposite CategoryTheory.Limits.hasCoproductsOfShape_opposite
-/

#print CategoryTheory.Limits.hasCoproductsOfShape_of_opposite /-
theorem hasCoproductsOfShape_of_opposite [HasProductsOfShape X Cᵒᵖ] : HasCoproductsOfShape X C :=
  haveI : has_limits_of_shape (discrete X)ᵒᵖ Cᵒᵖ :=
    has_limits_of_shape_of_equivalence (discrete.opposite X).symm
  has_colimits_of_shape_of_has_limits_of_shape_op
#align category_theory.limits.has_coproducts_of_shape_of_opposite CategoryTheory.Limits.hasCoproductsOfShape_of_opposite
-/

#print CategoryTheory.Limits.hasProductsOfShape_opposite /-
/-- If `C` has coproducts indexed by `X`, then `Cᵒᵖ` has products indexed by `X`.
-/
instance hasProductsOfShape_opposite [HasCoproductsOfShape X C] : HasProductsOfShape X Cᵒᵖ :=
  by
  haveI : has_colimits_of_shape (discrete X)ᵒᵖ C :=
    has_colimits_of_shape_of_equivalence (discrete.opposite X).symm
  infer_instance
#align category_theory.limits.has_products_of_shape_opposite CategoryTheory.Limits.hasProductsOfShape_opposite
-/

#print CategoryTheory.Limits.hasProductsOfShape_of_opposite /-
theorem hasProductsOfShape_of_opposite [HasCoproductsOfShape X Cᵒᵖ] : HasProductsOfShape X C :=
  haveI : has_colimits_of_shape (discrete X)ᵒᵖ Cᵒᵖ :=
    has_colimits_of_shape_of_equivalence (discrete.opposite X).symm
  has_limits_of_shape_of_has_colimits_of_shape_op
#align category_theory.limits.has_products_of_shape_of_opposite CategoryTheory.Limits.hasProductsOfShape_of_opposite
-/

#print CategoryTheory.Limits.hasProducts_opposite /-
instance hasProducts_opposite [HasCoproducts.{v₂} C] : HasProducts.{v₂} Cᵒᵖ := fun X =>
  inferInstance
#align category_theory.limits.has_products_opposite CategoryTheory.Limits.hasProducts_opposite
-/

#print CategoryTheory.Limits.hasProducts_of_opposite /-
theorem hasProducts_of_opposite [HasCoproducts.{v₂} Cᵒᵖ] : HasProducts.{v₂} C := fun X =>
  hasProductsOfShape_of_opposite X
#align category_theory.limits.has_products_of_opposite CategoryTheory.Limits.hasProducts_of_opposite
-/

#print CategoryTheory.Limits.hasCoproducts_opposite /-
instance hasCoproducts_opposite [HasProducts.{v₂} C] : HasCoproducts.{v₂} Cᵒᵖ := fun X =>
  inferInstance
#align category_theory.limits.has_coproducts_opposite CategoryTheory.Limits.hasCoproducts_opposite
-/

#print CategoryTheory.Limits.hasCoproducts_of_opposite /-
theorem hasCoproducts_of_opposite [HasProducts.{v₂} Cᵒᵖ] : HasCoproducts.{v₂} C := fun X =>
  hasCoproductsOfShape_of_opposite X
#align category_theory.limits.has_coproducts_of_opposite CategoryTheory.Limits.hasCoproducts_of_opposite
-/

#print CategoryTheory.Limits.hasFiniteCoproducts_opposite /-
instance hasFiniteCoproducts_opposite [HasFiniteProducts C] : HasFiniteCoproducts Cᵒᵖ
    where out n := Limits.hasCoproductsOfShape_opposite _
#align category_theory.limits.has_finite_coproducts_opposite CategoryTheory.Limits.hasFiniteCoproducts_opposite
-/

#print CategoryTheory.Limits.hasFiniteCoproducts_of_opposite /-
theorem hasFiniteCoproducts_of_opposite [HasFiniteProducts Cᵒᵖ] : HasFiniteCoproducts C :=
  { out := fun n => hasCoproductsOfShape_of_opposite _ }
#align category_theory.limits.has_finite_coproducts_of_opposite CategoryTheory.Limits.hasFiniteCoproducts_of_opposite
-/

#print CategoryTheory.Limits.hasFiniteProducts_opposite /-
instance hasFiniteProducts_opposite [HasFiniteCoproducts C] : HasFiniteProducts Cᵒᵖ
    where out n := inferInstance
#align category_theory.limits.has_finite_products_opposite CategoryTheory.Limits.hasFiniteProducts_opposite
-/

#print CategoryTheory.Limits.hasFiniteProducts_of_opposite /-
theorem hasFiniteProducts_of_opposite [HasFiniteCoproducts Cᵒᵖ] : HasFiniteProducts C :=
  { out := fun n => hasProductsOfShape_of_opposite _ }
#align category_theory.limits.has_finite_products_of_opposite CategoryTheory.Limits.hasFiniteProducts_of_opposite
-/

#print CategoryTheory.Limits.hasEqualizers_opposite /-
instance hasEqualizers_opposite [HasCoequalizers C] : HasEqualizers Cᵒᵖ :=
  by
  haveI : has_colimits_of_shape walking_parallel_pairᵒᵖ C :=
    has_colimits_of_shape_of_equivalence walking_parallel_pair_op_equiv
  infer_instance
#align category_theory.limits.has_equalizers_opposite CategoryTheory.Limits.hasEqualizers_opposite
-/

#print CategoryTheory.Limits.hasCoequalizers_opposite /-
instance hasCoequalizers_opposite [HasEqualizers C] : HasCoequalizers Cᵒᵖ :=
  by
  haveI : has_limits_of_shape walking_parallel_pairᵒᵖ C :=
    has_limits_of_shape_of_equivalence walking_parallel_pair_op_equiv
  infer_instance
#align category_theory.limits.has_coequalizers_opposite CategoryTheory.Limits.hasCoequalizers_opposite
-/

#print CategoryTheory.Limits.hasFiniteColimits_opposite /-
instance hasFiniteColimits_opposite [HasFiniteLimits C] : HasFiniteColimits Cᵒᵖ
    where out J 𝒟 𝒥 := by
    skip
    infer_instance
#align category_theory.limits.has_finite_colimits_opposite CategoryTheory.Limits.hasFiniteColimits_opposite
-/

#print CategoryTheory.Limits.hasFiniteLimits_opposite /-
instance hasFiniteLimits_opposite [HasFiniteColimits C] : HasFiniteLimits Cᵒᵖ
    where out J 𝒟 𝒥 := by
    skip
    infer_instance
#align category_theory.limits.has_finite_limits_opposite CategoryTheory.Limits.hasFiniteLimits_opposite
-/

#print CategoryTheory.Limits.hasPullbacks_opposite /-
instance hasPullbacks_opposite [HasPushouts C] : HasPullbacks Cᵒᵖ :=
  by
  haveI : has_colimits_of_shape walking_cospanᵒᵖ C :=
    has_colimits_of_shape_of_equivalence walking_cospan_op_equiv.symm
  apply has_limits_of_shape_op_of_has_colimits_of_shape
#align category_theory.limits.has_pullbacks_opposite CategoryTheory.Limits.hasPullbacks_opposite
-/

#print CategoryTheory.Limits.hasPushouts_opposite /-
instance hasPushouts_opposite [HasPullbacks C] : HasPushouts Cᵒᵖ :=
  by
  haveI : has_limits_of_shape walking_spanᵒᵖ C :=
    has_limits_of_shape_of_equivalence walking_span_op_equiv.symm
  infer_instance
#align category_theory.limits.has_pushouts_opposite CategoryTheory.Limits.hasPushouts_opposite
-/

#print CategoryTheory.Limits.spanOp /-
/-- The canonical isomorphism relating `span f.op g.op` and `(cospan f g).op` -/
@[simps]
def spanOp {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) :
    span f.op g.op ≅ walkingCospanOpEquiv.inverse ⋙ (cospan f g).op :=
  NatIso.ofComponents (by rintro (_ | _ | _) <;> rfl)
    (by rintro (_ | _ | _) (_ | _ | _) f <;> cases f <;> tidy)
#align category_theory.limits.span_op CategoryTheory.Limits.spanOp
-/

#print CategoryTheory.Limits.opCospan /-
/-- The canonical isomorphism relating `(cospan f g).op` and `span f.op g.op` -/
@[simps]
def opCospan {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) :
    (cospan f g).op ≅ walkingCospanOpEquiv.Functor ⋙ span f.op g.op :=
  calc
    (cospan f g).op ≅ 𝟭 _ ⋙ (cospan f g).op := by rfl
    _ ≅ (walkingCospanOpEquiv.Functor ⋙ walkingCospanOpEquiv.inverse) ⋙ (cospan f g).op :=
      (isoWhiskerRight walkingCospanOpEquiv.unitIso _)
    _ ≅ walkingCospanOpEquiv.Functor ⋙ walkingCospanOpEquiv.inverse ⋙ (cospan f g).op :=
      (Functor.associator _ _ _)
    _ ≅ walkingCospanOpEquiv.Functor ⋙ span f.op g.op := isoWhiskerLeft _ (spanOp f g).symm

#align category_theory.limits.op_cospan CategoryTheory.Limits.opCospan
-/

#print CategoryTheory.Limits.cospanOp /-
/-- The canonical isomorphism relating `cospan f.op g.op` and `(span f g).op` -/
@[simps]
def cospanOp {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) :
    cospan f.op g.op ≅ walkingSpanOpEquiv.inverse ⋙ (span f g).op :=
  NatIso.ofComponents (by rintro (_ | _ | _) <;> rfl)
    (by rintro (_ | _ | _) (_ | _ | _) f <;> cases f <;> tidy)
#align category_theory.limits.cospan_op CategoryTheory.Limits.cospanOp
-/

#print CategoryTheory.Limits.opSpan /-
/-- The canonical isomorphism relating `(span f g).op` and `cospan f.op g.op` -/
@[simps]
def opSpan {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) :
    (span f g).op ≅ walkingSpanOpEquiv.Functor ⋙ cospan f.op g.op :=
  calc
    (span f g).op ≅ 𝟭 _ ⋙ (span f g).op := by rfl
    _ ≅ (walkingSpanOpEquiv.Functor ⋙ walkingSpanOpEquiv.inverse) ⋙ (span f g).op :=
      (isoWhiskerRight walkingSpanOpEquiv.unitIso _)
    _ ≅ walkingSpanOpEquiv.Functor ⋙ walkingSpanOpEquiv.inverse ⋙ (span f g).op :=
      (Functor.associator _ _ _)
    _ ≅ walkingSpanOpEquiv.Functor ⋙ cospan f.op g.op := isoWhiskerLeft _ (cospanOp f g).symm

#align category_theory.limits.op_span CategoryTheory.Limits.opSpan
-/

namespace PushoutCocone

#print CategoryTheory.Limits.PushoutCocone.unop /-
/-- The obvious map `pushout_cocone f g → pullback_cone f.unop g.unop` -/
@[simps (config := lemmasOnly)]
def unop {X Y Z : Cᵒᵖ} {f : X ⟶ Y} {g : X ⟶ Z} (c : PushoutCocone f g) :
    PullbackCone f.unop g.unop :=
  Cocone.unop
    ((Cocones.precompose (opCospan f.unop g.unop).hom).obj
      (Cocone.whisker walkingCospanOpEquiv.Functor c))
#align category_theory.limits.pushout_cocone.unop CategoryTheory.Limits.PushoutCocone.unop
-/

#print CategoryTheory.Limits.PushoutCocone.unop_fst /-
@[simp]
theorem unop_fst {X Y Z : Cᵒᵖ} {f : X ⟶ Y} {g : X ⟶ Z} (c : PushoutCocone f g) :
    c.unop.fst = c.inl.unop :=
  by
  change (_ : limits.cone _).π.app _ = _
  simp only [pushout_cocone.ι_app_left, pushout_cocone.unop_π_app]
  tidy
#align category_theory.limits.pushout_cocone.unop_fst CategoryTheory.Limits.PushoutCocone.unop_fst
-/

#print CategoryTheory.Limits.PushoutCocone.unop_snd /-
@[simp]
theorem unop_snd {X Y Z : Cᵒᵖ} {f : X ⟶ Y} {g : X ⟶ Z} (c : PushoutCocone f g) :
    c.unop.snd = c.inr.unop :=
  by
  change (_ : limits.cone _).π.app _ = _
  simp only [pushout_cocone.unop_π_app, pushout_cocone.ι_app_right]
  tidy
#align category_theory.limits.pushout_cocone.unop_snd CategoryTheory.Limits.PushoutCocone.unop_snd
-/

#print CategoryTheory.Limits.PushoutCocone.op /-
/-- The obvious map `pushout_cocone f.op g.op → pullback_cone f g` -/
@[simps (config := lemmasOnly)]
def op {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} (c : PushoutCocone f g) : PullbackCone f.op g.op :=
  (Cones.postcompose (cospanOp f g).symm.hom).obj
    (Cone.whisker walkingSpanOpEquiv.inverse (Cocone.op c))
#align category_theory.limits.pushout_cocone.op CategoryTheory.Limits.PushoutCocone.op
-/

#print CategoryTheory.Limits.PushoutCocone.op_fst /-
@[simp]
theorem op_fst {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} (c : PushoutCocone f g) : c.op.fst = c.inl.op :=
  by
  change (_ : limits.cone _).π.app _ = _
  apply category.comp_id
#align category_theory.limits.pushout_cocone.op_fst CategoryTheory.Limits.PushoutCocone.op_fst
-/

#print CategoryTheory.Limits.PushoutCocone.op_snd /-
@[simp]
theorem op_snd {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} (c : PushoutCocone f g) : c.op.snd = c.inr.op :=
  by
  change (_ : limits.cone _).π.app _ = _
  apply category.comp_id
#align category_theory.limits.pushout_cocone.op_snd CategoryTheory.Limits.PushoutCocone.op_snd
-/

end PushoutCocone

namespace PullbackCone

#print CategoryTheory.Limits.PullbackCone.unop /-
/-- The obvious map `pullback_cone f g → pushout_cocone f.unop g.unop` -/
@[simps (config := lemmasOnly)]
def unop {X Y Z : Cᵒᵖ} {f : X ⟶ Z} {g : Y ⟶ Z} (c : PullbackCone f g) :
    PushoutCocone f.unop g.unop :=
  Cone.unop
    ((Cones.postcompose (opSpan f.unop g.unop).symm.hom).obj
      (Cone.whisker walkingSpanOpEquiv.Functor c))
#align category_theory.limits.pullback_cone.unop CategoryTheory.Limits.PullbackCone.unop
-/

#print CategoryTheory.Limits.PullbackCone.unop_inl /-
@[simp]
theorem unop_inl {X Y Z : Cᵒᵖ} {f : X ⟶ Z} {g : Y ⟶ Z} (c : PullbackCone f g) :
    c.unop.inl = c.fst.unop :=
  by
  change (_ : limits.cocone _).ι.app _ = _
  dsimp only [unop, op_span]
  simp; dsimp; simp; dsimp; simp
#align category_theory.limits.pullback_cone.unop_inl CategoryTheory.Limits.PullbackCone.unop_inl
-/

#print CategoryTheory.Limits.PullbackCone.unop_inr /-
@[simp]
theorem unop_inr {X Y Z : Cᵒᵖ} {f : X ⟶ Z} {g : Y ⟶ Z} (c : PullbackCone f g) :
    c.unop.inr = c.snd.unop :=
  by
  change (_ : limits.cocone _).ι.app _ = _
  apply Quiver.Hom.op_inj
  simp [unop_ι_app]; dsimp; simp
  apply category.comp_id
#align category_theory.limits.pullback_cone.unop_inr CategoryTheory.Limits.PullbackCone.unop_inr
-/

#print CategoryTheory.Limits.PullbackCone.op /-
/-- The obvious map `pullback_cone f g → pushout_cocone f.op g.op` -/
@[simps (config := lemmasOnly)]
def op {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} (c : PullbackCone f g) : PushoutCocone f.op g.op :=
  (Cocones.precompose (spanOp f g).hom).obj
    (Cocone.whisker walkingCospanOpEquiv.inverse (Cone.op c))
#align category_theory.limits.pullback_cone.op CategoryTheory.Limits.PullbackCone.op
-/

#print CategoryTheory.Limits.PullbackCone.op_inl /-
@[simp]
theorem op_inl {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} (c : PullbackCone f g) : c.op.inl = c.fst.op :=
  by
  change (_ : limits.cocone _).ι.app _ = _
  apply category.id_comp
#align category_theory.limits.pullback_cone.op_inl CategoryTheory.Limits.PullbackCone.op_inl
-/

#print CategoryTheory.Limits.PullbackCone.op_inr /-
@[simp]
theorem op_inr {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} (c : PullbackCone f g) : c.op.inr = c.snd.op :=
  by
  change (_ : limits.cocone _).ι.app _ = _
  apply category.id_comp
#align category_theory.limits.pullback_cone.op_inr CategoryTheory.Limits.PullbackCone.op_inr
-/

#print CategoryTheory.Limits.PullbackCone.opUnop /-
/-- If `c` is a pullback cone, then `c.op.unop` is isomorphic to `c`. -/
def opUnop {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} (c : PullbackCone f g) : c.op.unop ≅ c :=
  PullbackCone.ext (Iso.refl _) (by simp) (by simp)
#align category_theory.limits.pullback_cone.op_unop CategoryTheory.Limits.PullbackCone.opUnop
-/

#print CategoryTheory.Limits.PullbackCone.unopOp /-
/-- If `c` is a pullback cone in `Cᵒᵖ`, then `c.unop.op` is isomorphic to `c`. -/
def unopOp {X Y Z : Cᵒᵖ} {f : X ⟶ Z} {g : Y ⟶ Z} (c : PullbackCone f g) : c.unop.op ≅ c :=
  PullbackCone.ext (Iso.refl _) (by simp) (by simp)
#align category_theory.limits.pullback_cone.unop_op CategoryTheory.Limits.PullbackCone.unopOp
-/

end PullbackCone

namespace PushoutCocone

#print CategoryTheory.Limits.PushoutCocone.opUnop /-
/-- If `c` is a pushout cocone, then `c.op.unop` is isomorphic to `c`. -/
def opUnop {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} (c : PushoutCocone f g) : c.op.unop ≅ c :=
  PushoutCocone.ext (Iso.refl _) (by simp) (by simp)
#align category_theory.limits.pushout_cocone.op_unop CategoryTheory.Limits.PushoutCocone.opUnop
-/

#print CategoryTheory.Limits.PushoutCocone.unopOp /-
/-- If `c` is a pushout cocone in `Cᵒᵖ`, then `c.unop.op` is isomorphic to `c`. -/
def unopOp {X Y Z : Cᵒᵖ} {f : X ⟶ Y} {g : X ⟶ Z} (c : PushoutCocone f g) : c.unop.op ≅ c :=
  PushoutCocone.ext (Iso.refl _) (by simp) (by simp)
#align category_theory.limits.pushout_cocone.unop_op CategoryTheory.Limits.PushoutCocone.unopOp
-/

#print CategoryTheory.Limits.PushoutCocone.isColimitEquivIsLimitOp /-
/-- A pushout cone is a colimit cocone if and only if the corresponding pullback cone
in the opposite category is a limit cone. -/
def isColimitEquivIsLimitOp {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} (c : PushoutCocone f g) :
    IsColimit c ≃ IsLimit c.op :=
  by
  apply equivOfSubsingletonOfSubsingleton
  · intro h
    equiv_rw is_limit.postcompose_hom_equiv _ _
    equiv_rw(is_limit.whisker_equivalence_equiv walking_span_op_equiv.symm).symm
    exact is_limit_cocone_op _ h
  · intro h
    equiv_rw is_colimit.equiv_iso_colimit c.op_unop.symm
    apply is_colimit_cone_unop
    equiv_rw is_limit.postcompose_hom_equiv _ _
    equiv_rw(is_limit.whisker_equivalence_equiv _).symm
    exact h
#align category_theory.limits.pushout_cocone.is_colimit_equiv_is_limit_op CategoryTheory.Limits.PushoutCocone.isColimitEquivIsLimitOp
-/

#print CategoryTheory.Limits.PushoutCocone.isColimitEquivIsLimitUnop /-
/-- A pushout cone is a colimit cocone in `Cᵒᵖ` if and only if the corresponding pullback cone
in `C` is a limit cone. -/
def isColimitEquivIsLimitUnop {X Y Z : Cᵒᵖ} {f : X ⟶ Y} {g : X ⟶ Z} (c : PushoutCocone f g) :
    IsColimit c ≃ IsLimit c.unop :=
  by
  apply equivOfSubsingletonOfSubsingleton
  · intro h
    apply is_limit_cocone_unop
    equiv_rw is_colimit.precompose_hom_equiv _ _
    equiv_rw(is_colimit.whisker_equivalence_equiv _).symm
    exact h
  · intro h
    equiv_rw is_colimit.equiv_iso_colimit c.unop_op.symm
    equiv_rw is_colimit.precompose_hom_equiv _ _
    equiv_rw(is_colimit.whisker_equivalence_equiv walking_cospan_op_equiv.symm).symm
    exact is_colimit_cone_op _ h
#align category_theory.limits.pushout_cocone.is_colimit_equiv_is_limit_unop CategoryTheory.Limits.PushoutCocone.isColimitEquivIsLimitUnop
-/

end PushoutCocone

namespace PullbackCone

#print CategoryTheory.Limits.PullbackCone.isLimitEquivIsColimitOp /-
/-- A pullback cone is a limit cone if and only if the corresponding pushout cocone
in the opposite category is a colimit cocone. -/
def isLimitEquivIsColimitOp {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} (c : PullbackCone f g) :
    IsLimit c ≃ IsColimit c.op :=
  (IsLimit.equivIsoLimit c.op_unop).symm.trans c.op.isColimitEquivIsLimitUnop.symm
#align category_theory.limits.pullback_cone.is_limit_equiv_is_colimit_op CategoryTheory.Limits.PullbackCone.isLimitEquivIsColimitOp
-/

#print CategoryTheory.Limits.PullbackCone.isLimitEquivIsColimitUnop /-
/-- A pullback cone is a limit cone in `Cᵒᵖ` if and only if the corresponding pushout cocone
in `C` is a colimit cocone. -/
def isLimitEquivIsColimitUnop {X Y Z : Cᵒᵖ} {f : X ⟶ Z} {g : Y ⟶ Z} (c : PullbackCone f g) :
    IsLimit c ≃ IsColimit c.unop :=
  (IsLimit.equivIsoLimit c.unop_op).symm.trans c.unop.isColimitEquivIsLimitOp.symm
#align category_theory.limits.pullback_cone.is_limit_equiv_is_colimit_unop CategoryTheory.Limits.PullbackCone.isLimitEquivIsColimitUnop
-/

end PullbackCone

section Pullback

open Opposite

#print CategoryTheory.Limits.pullbackIsoUnopPushout /-
/-- The pullback of `f` and `g` in `C` is isomorphic to the pushout of
`f.op` and `g.op` in `Cᵒᵖ`. -/
noncomputable def pullbackIsoUnopPushout {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g]
    [HasPushout f.op g.op] : pullback f g ≅ unop (pushout f.op g.op) :=
  IsLimit.conePointUniqueUpToIso (limit.isLimit _)
    ((PushoutCocone.isColimitEquivIsLimitUnop _) (colimit.isColimit (span f.op g.op)))
#align category_theory.limits.pullback_iso_unop_pushout CategoryTheory.Limits.pullbackIsoUnopPushout
-/

#print CategoryTheory.Limits.pullbackIsoUnopPushout_inv_fst /-
@[simp, reassoc.1]
theorem pullbackIsoUnopPushout_inv_fst {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g]
    [HasPushout f.op g.op] :
    (pullbackIsoUnopPushout f g).inv ≫ pullback.fst = (pushout.inl : _ ⟶ pushout f.op g.op).unop :=
  (IsLimit.conePointUniqueUpToIso_inv_comp _ _ _).trans (by simp)
#align category_theory.limits.pullback_iso_unop_pushout_inv_fst CategoryTheory.Limits.pullbackIsoUnopPushout_inv_fst
-/

#print CategoryTheory.Limits.pullbackIsoUnopPushout_inv_snd /-
@[simp, reassoc.1]
theorem pullbackIsoUnopPushout_inv_snd {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g]
    [HasPushout f.op g.op] :
    (pullbackIsoUnopPushout f g).inv ≫ pullback.snd = (pushout.inr : _ ⟶ pushout f.op g.op).unop :=
  (IsLimit.conePointUniqueUpToIso_inv_comp _ _ _).trans (by simp)
#align category_theory.limits.pullback_iso_unop_pushout_inv_snd CategoryTheory.Limits.pullbackIsoUnopPushout_inv_snd
-/

#print CategoryTheory.Limits.pullbackIsoUnopPushout_hom_inl /-
@[simp, reassoc.1]
theorem pullbackIsoUnopPushout_hom_inl {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g]
    [HasPushout f.op g.op] : pushout.inl ≫ (pullbackIsoUnopPushout f g).hom.op = pullback.fst.op :=
  by
  apply Quiver.Hom.unop_inj
  dsimp
  rw [← pullback_iso_unop_pushout_inv_fst, iso.hom_inv_id_assoc]
#align category_theory.limits.pullback_iso_unop_pushout_hom_inl CategoryTheory.Limits.pullbackIsoUnopPushout_hom_inl
-/

#print CategoryTheory.Limits.pullbackIsoUnopPushout_hom_inr /-
@[simp, reassoc.1]
theorem pullbackIsoUnopPushout_hom_inr {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g]
    [HasPushout f.op g.op] : pushout.inr ≫ (pullbackIsoUnopPushout f g).hom.op = pullback.snd.op :=
  by
  apply Quiver.Hom.unop_inj
  dsimp
  rw [← pullback_iso_unop_pushout_inv_snd, iso.hom_inv_id_assoc]
#align category_theory.limits.pullback_iso_unop_pushout_hom_inr CategoryTheory.Limits.pullbackIsoUnopPushout_hom_inr
-/

end Pullback

section Pushout

#print CategoryTheory.Limits.pushoutIsoUnopPullback /-
/-- The pushout of `f` and `g` in `C` is isomorphic to the pullback of
 `f.op` and `g.op` in `Cᵒᵖ`. -/
noncomputable def pushoutIsoUnopPullback {X Y Z : C} (f : X ⟶ Z) (g : X ⟶ Y) [HasPushout f g]
    [HasPullback f.op g.op] : pushout f g ≅ unop (pullback f.op g.op) :=
  IsColimit.coconePointUniqueUpToIso (colimit.isColimit _)
    ((PullbackCone.isLimitEquivIsColimitUnop _) (limit.isLimit (cospan f.op g.op)))
#align category_theory.limits.pushout_iso_unop_pullback CategoryTheory.Limits.pushoutIsoUnopPullback
-/

#print CategoryTheory.Limits.pushoutIsoUnopPullback_inl_hom /-
@[simp, reassoc.1]
theorem pushoutIsoUnopPullback_inl_hom {X Y Z : C} (f : X ⟶ Z) (g : X ⟶ Y) [HasPushout f g]
    [HasPullback f.op g.op] :
    pushout.inl ≫ (pushoutIsoUnopPullback f g).hom = (pullback.fst : pullback f.op g.op ⟶ _).unop :=
  (IsColimit.comp_coconePointUniqueUpToIso_hom _ _ _).trans (by simp)
#align category_theory.limits.pushout_iso_unop_pullback_inl_hom CategoryTheory.Limits.pushoutIsoUnopPullback_inl_hom
-/

#print CategoryTheory.Limits.pushoutIsoUnopPullback_inr_hom /-
@[simp, reassoc.1]
theorem pushoutIsoUnopPullback_inr_hom {X Y Z : C} (f : X ⟶ Z) (g : X ⟶ Y) [HasPushout f g]
    [HasPullback f.op g.op] :
    pushout.inr ≫ (pushoutIsoUnopPullback f g).hom = (pullback.snd : pullback f.op g.op ⟶ _).unop :=
  (IsColimit.comp_coconePointUniqueUpToIso_hom _ _ _).trans (by simp)
#align category_theory.limits.pushout_iso_unop_pullback_inr_hom CategoryTheory.Limits.pushoutIsoUnopPullback_inr_hom
-/

#print CategoryTheory.Limits.pushoutIsoUnopPullback_inv_fst /-
@[simp]
theorem pushoutIsoUnopPullback_inv_fst {X Y Z : C} (f : X ⟶ Z) (g : X ⟶ Y) [HasPushout f g]
    [HasPullback f.op g.op] : (pushoutIsoUnopPullback f g).inv.op ≫ pullback.fst = pushout.inl.op :=
  by
  apply Quiver.Hom.unop_inj
  dsimp
  rw [← pushout_iso_unop_pullback_inl_hom, category.assoc, iso.hom_inv_id, category.comp_id]
#align category_theory.limits.pushout_iso_unop_pullback_inv_fst CategoryTheory.Limits.pushoutIsoUnopPullback_inv_fst
-/

#print CategoryTheory.Limits.pushoutIsoUnopPullback_inv_snd /-
@[simp]
theorem pushoutIsoUnopPullback_inv_snd {X Y Z : C} (f : X ⟶ Z) (g : X ⟶ Y) [HasPushout f g]
    [HasPullback f.op g.op] : (pushoutIsoUnopPullback f g).inv.op ≫ pullback.snd = pushout.inr.op :=
  by
  apply Quiver.Hom.unop_inj
  dsimp
  rw [← pushout_iso_unop_pullback_inr_hom, category.assoc, iso.hom_inv_id, category.comp_id]
#align category_theory.limits.pushout_iso_unop_pullback_inv_snd CategoryTheory.Limits.pushoutIsoUnopPullback_inv_snd
-/

end Pushout

end CategoryTheory.Limits

author: leanprover-community


text:
/-
Copyright (c) 2018 Kenny Lau. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kenny Lau

! This file was ported from Lean 3 source module algebra.field.opposite
! leanprover-community/mathlib commit 76de8ae01554c3b37d66544866659ff174e66e1f
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathbin.Algebra.Field.Defs
import Mathbin.Algebra.Ring.Opposite
import Mathbin.Data.Int.Cast.Lemmas

/-!
# Field structure on the multiplicative/additive opposite

> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
> Any changes to this file require a corresponding PR to mathlib4.
-/

variable (α : Type _)

namespace MulOpposite

@[to_additive]
instance [HasRatCast α] : HasRatCast αᵐᵒᵖ :=
  ⟨fun n => op n⟩

variable {α}

/- warning: mul_opposite.op_rat_cast -> MulOpposite.op_ratCast is a dubious translation:
lean 3 declaration is
  forall {α : Type.{u1}} [_inst_1 : HasRatCast.{u1} α] (q : Rat), Eq.{succ u1} (MulOpposite.{u1} α) (MulOpposite.op.{u1} α ((fun (a : Type) (b : Type.{u1}) [self : HasLiftT.{1, succ u1} a b] => self.0) Rat α (HasLiftT.mk.{1, succ u1} Rat α (CoeTCₓ.coe.{1, succ u1} Rat α (Rat.castCoe.{u1} α _inst_1))) q)) ((fun (a : Type) (b : Type.{u1}) [self : HasLiftT.{1, succ u1} a b] => self.0) Rat (MulOpposite.{u1} α) (HasLiftT.mk.{1, succ u1} Rat (MulOpposite.{u1} α) (CoeTCₓ.coe.{1, succ u1} Rat (MulOpposite.{u1} α) (Rat.castCoe.{u1} (MulOpposite.{u1} α) (MulOpposite.hasRatCast.{u1} α _inst_1)))) q)
but is expected to have type
  forall {α : Type.{u1}} [_inst_1 : RatCast.{u1} α] (q : Rat), Eq.{succ u1} (MulOpposite.{u1} α) (MulOpposite.op.{u1} α (Rat.cast.{u1} α _inst_1 q)) (Rat.cast.{u1} (MulOpposite.{u1} α) (MulOpposite.ratCast.{u1} α _inst_1) q)
Case conversion may be inaccurate. Consider using '#align mul_opposite.op_rat_cast MulOpposite.op_ratCastₓ'. -/
@[simp, norm_cast, to_additive]
theorem op_ratCast [HasRatCast α] (q : ℚ) : op (q : α) = q :=
  rfl
#align mul_opposite.op_rat_cast MulOpposite.op_ratCast
#align add_opposite.op_rat_cast AddOpposite.op_ratCast

/- warning: mul_opposite.unop_rat_cast -> MulOpposite.unop_ratCast is a dubious translation:
lean 3 declaration is
  forall {α : Type.{u1}} [_inst_1 : HasRatCast.{u1} α] (q : Rat), Eq.{succ u1} α (MulOpposite.unop.{u1} α ((fun (a : Type) (b : Type.{u1}) [self : HasLiftT.{1, succ u1} a b] => self.0) Rat (MulOpposite.{u1} α) (HasLiftT.mk.{1, succ u1} Rat (MulOpposite.{u1} α) (CoeTCₓ.coe.{1, succ u1} Rat (MulOpposite.{u1} α) (Rat.castCoe.{u1} (MulOpposite.{u1} α) (MulOpposite.hasRatCast.{u1} α _inst_1)))) q)) ((fun (a : Type) (b : Type.{u1}) [self : HasLiftT.{1, succ u1} a b] => self.0) Rat α (HasLiftT.mk.{1, succ u1} Rat α (CoeTCₓ.coe.{1, succ u1} Rat α (Rat.castCoe.{u1} α _inst_1))) q)
but is expected to have type
  forall {α : Type.{u1}} [_inst_1 : RatCast.{u1} α] (q : Rat), Eq.{succ u1} α (MulOpposite.unop.{u1} α (Rat.cast.{u1} (MulOpposite.{u1} α) (MulOpposite.ratCast.{u1} α _inst_1) q)) (Rat.cast.{u1} α _inst_1 q)
Case conversion may be inaccurate. Consider using '#align mul_opposite.unop_rat_cast MulOpposite.unop_ratCastₓ'. -/
@[simp, norm_cast, to_additive]
theorem unop_ratCast [HasRatCast α] (q : ℚ) : unop (q : αᵐᵒᵖ) = q :=
  rfl
#align mul_opposite.unop_rat_cast MulOpposite.unop_ratCast
#align add_opposite.unop_rat_cast AddOpposite.unop_ratCast

variable (α)

instance [DivisionSemiring α] : DivisionSemiring αᵐᵒᵖ :=
  { MulOpposite.groupWithZero α, MulOpposite.semiring α with }

instance [DivisionRing α] : DivisionRing αᵐᵒᵖ :=
  { MulOpposite.divisionSemiring α,
    MulOpposite.ring α with
    ratCast := fun q => op q
    ratCast_mk := fun a b hb h =>
      by
      rw [Rat.cast_def, op_div, op_nat_cast, op_int_cast]
      exact Int.commute_cast _ _ }

instance [Semifield α] : Semifield αᵐᵒᵖ :=
  { MulOpposite.divisionSemiring α, MulOpposite.commSemiring α with }

instance [Field α] : Field αᵐᵒᵖ :=
  { MulOpposite.divisionRing α, MulOpposite.commRing α with }

end MulOpposite

namespace AddOpposite

instance [DivisionSemiring α] : DivisionSemiring αᵃᵒᵖ :=
  { AddOpposite.groupWithZero α, AddOpposite.semiring α with }

instance [DivisionRing α] : DivisionRing αᵃᵒᵖ :=
  { AddOpposite.ring α, AddOpposite.groupWithZero α, AddOpposite.hasRatCast α with
    ratCast_mk := fun a b hb h => by rw [← div_eq_mul_inv] <;> exact congr_arg op (Rat.cast_def _) }

instance [Semifield α] : Semifield αᵃᵒᵖ :=
  { AddOpposite.divisionSemiring α, AddOpposite.commSemiring α with }

instance [Field α] : Field αᵃᵒᵖ :=
  { AddOpposite.divisionRing α, AddOpposite.commRing α with }

end AddOpposite


text:
import category_theory.limits.preserves.limits
import for_mathlib.derived.K_projective
import for_mathlib.AddCommGroup.explicit_limits

open category_theory
open category_theory.limits

universes v u
variables {A : Type u} [category.{v} A] [abelian A] [has_coproducts A]

open_locale zero_object

namespace category_theory

instance is_iso_coproduct {α : Type v} (X Y : α → A) (f : Π a, X a ⟶ Y a)
  [∀ a, is_iso (f a)] :
  is_iso (sigma.desc $ λ a, f a ≫ sigma.ι _ a) :=
begin
  use sigma.desc (λ a, inv (f a) ≫ sigma.ι _ a),
  split,
  { ext, dsimp, simp },
  { ext, dsimp, simp }
end

noncomputable
lemma is_initial_colimit {J : Type v} [small_category J] (K : J ⥤ A)
  (hK : ∀ j, is_initial (K.obj j)) [has_colimit K] :
  is_initial (colimit K) :=
{ desc := λ T, colimit.desc _ ⟨_,
  { app := λ j, (hK j).to _,
    naturality' := λ i j f, (hK _).hom_ext _ _ }⟩,
  fac' := by rintros S ⟨⟩,
  uniq' := begin
    intros S m hm, apply colimit.hom_ext, intros j,
    apply (hK _).hom_ext
  end }

lemma is_zero_colimit {J : Type v} [small_category J] (K : J ⥤ A)
  (hK : ∀ j, is_zero (K.obj j)) [has_colimit K] :
  is_zero (colimit K) :=
begin
  suffices : is_initial (colimit K),
  { let e : colimit K ≅ ⊥_ _ := (initial_iso_is_initial this).symm,
    apply is_zero_of_iso_of_zero _ e.symm,
    apply is_zero_initial },
  apply is_initial_colimit,
  intros j,
  apply is_zero.is_initial,
  apply hK,
end

noncomputable
def preadditive_yoneda_coproduct_to_product {A : Type u} [category.{v} A]
  [preadditive A]
  {α : Type v} (X : α → A) [has_coproduct X] (Y : A) :
  (preadditive_yoneda.obj Y).obj (opposite.op $ sigma_obj X) ⟶
  pi_obj (λ a, (preadditive_yoneda.obj Y).obj (opposite.op $ X a)) :=
pi.lift $ λ b, functor.map _ $ quiver.hom.op $ sigma.ι _ _

set_option pp.universes true

instance is_iso_preadditive_yoneda_coproduct_to_product
  {A : Type u} [category.{v} A]
  [preadditive A]
  {α : Type v} (X : α → A) [has_coproduct X] (Y : A) :
  is_iso (preadditive_yoneda_coproduct_to_product X Y) :=
begin
  apply is_iso_of_reflects_iso _ (forget AddCommGroup),
  rw is_iso_iff_bijective,
  split,
  { intros f g h, dsimp [preadditive_yoneda_coproduct_to_product] at f g h ⊢,
    apply colimit.hom_ext,
    intros a,
    let q : (∏ λ (a : α), AddCommGroup.of (X a ⟶ Y)) ⟶ (AddCommGroup.of (X a ⟶ Y)) :=
      pi.π _ a,
    apply_fun (λ e, q e) at h,
    simp only [← comp_apply, limit.lift_π] at h, exact h },
  { intros f, dsimp at f,
    let P : Π a, (∏ λ (a : α), AddCommGroup.of (X a ⟶ Y)) ⟶ (AddCommGroup.of (X a ⟶ Y)) :=
      λ a, pi.π _ a,
    let q : sigma_obj X ⟶ Y := sigma.desc (λ a, P a f),
    use q,
    apply concrete.limit_ext (discrete.functor (λ a, AddCommGroup.of (X a ⟶ Y))),
    intros i, dsimp [preadditive_yoneda_coproduct_to_product],
    simp only [← comp_apply, limit.lift_π],
    dsimp, rw colimit.ι_desc, refl }
end

noncomputable
def preadditive_yoneda_coproduct_iso {A : Type u} [category.{v} A]
  [preadditive A]
  {α : Type v} (X : α → A) [has_coproduct X] (Y : A) :
  (preadditive_yoneda.obj Y).obj (opposite.op $ sigma_obj X) ≅
  pi_obj (λ a, (preadditive_yoneda.obj Y).obj (opposite.op $ X a)) :=
as_iso (preadditive_yoneda_coproduct_to_product _ _)

noncomputable
def pi_iso {A : Type u} [category.{v} A] {α : Type v}
  (X Y : α → A)
  (I : Π a, X a ≅ Y a)
  [has_product X] [has_product Y] :
  pi_obj X ≅ pi_obj Y :=
{ hom := pi.lift $ λ b, pi.π _ _ ≫ (I b).hom,
  inv := pi.lift $ λ b, pi.π _ _ ≫ (I b).inv,
  hom_inv_id' := begin
    apply limit.hom_ext, intros i,
    simp,
  end,
  inv_hom_id' := begin
    apply limit.hom_ext, intros i,
    simp,
  end }

end category_theory

namespace homotopy_category

noncomputable
def coproduct_iso {α : Type v} (X : α → cochain_complex A ℤ) (i) :
  (sigma_obj X).X i ≅ sigma_obj (λ a : α, (X a).X i) :=
(category_theory.preserves_colimit_iso (homological_complex.eval A
  (complex_shape.up ℤ) i) (discrete.functor X)) ≪≫
  has_colimit.iso_of_nat_iso
  (nat_iso.of_components (λ _, iso.refl _) begin
    rintros i _ ⟨⟨⟨⟩⟩⟩,
    simp,
  end)

@[simp, reassoc]
lemma coproduct_ι_coproduct_iso_inv {α : Type v} (X : α → cochain_complex A ℤ) (i) (a) :
  sigma.ι _ a ≫ (coproduct_iso X i).inv = ((sigma.ι X a : _ ⟶ _)).f i :=
begin
  dsimp [coproduct_iso, has_colimit.iso_of_nat_iso,
    is_colimit.map, preserves_colimit_iso, is_colimit.cocone_point_unique_up_to_iso],
  simp, dsimp, simp,
end

@[simp, reassoc]
lemma coproduct_ι_coproduct_iso_hom {α : Type v} (X : α → cochain_complex A ℤ) (i) (a : α) :
  (sigma.ι X a : _ ⟶ _).f i ≫ (coproduct_iso X i).hom = sigma.ι _ a :=
begin
  dsimp [coproduct_iso, has_colimit.iso_of_nat_iso,
    is_colimit.map, preserves_colimit_iso, is_colimit.cocone_point_unique_up_to_iso],
  slice_lhs 0 1
  { erw (is_colimit_of_preserves (homological_complex.eval A (complex_shape.up ℤ) i)
    (colimit.is_colimit (discrete.functor X))).fac },
  simp, dsimp, simp,
end

noncomputable
def homotopy_coprod {α : Type v} (X : α → cochain_complex A ℤ) (Y)
  (f g : sigma_obj X ⟶ Y)
  (h : Π a, homotopy (sigma.ι _ a ≫ f) (sigma.ι _ a ≫ g)) :
  homotopy f g :=
{ hom := λ i j, (coproduct_iso X i).hom ≫
    (sigma.desc $ λ a, (h a).hom _ _),
  zero' := begin
    intros i j hh,
    simp only [preadditive.is_iso.comp_left_eq_zero],
    apply colimit.hom_ext, intros a,
    simp only [colimit.ι_desc, cofan.mk_ι_app, comp_zero, (h a).zero' i j hh],
  end,
  comm := begin
    intros i,
    rw ← cancel_epi (coproduct_iso X i).inv,
    apply colimit.hom_ext, intros a,
    simp only [coproduct_ι_coproduct_iso_inv_assoc, homological_complex.cochain_complex_d_next,
      homological_complex.cochain_complex_prev_d, category.assoc, preadditive.comp_add,
      homological_complex.hom.comm_assoc, coproduct_ι_coproduct_iso_hom_assoc,
      colimit.ι_desc, cofan.mk_ι_app, colimit.ι_desc_assoc],
    have := (h a).comm i,
    dsimp at this,
    rw this,
    simp only [homological_complex.cochain_complex_d_next,
      homological_complex.cochain_complex_prev_d],
  end }

lemma homotopic_coprod {α : Type v} (X : α → cochain_complex A ℤ) (Y)
  (f g : sigma_obj X ⟶ Y)
  (h : ∀ a : α, homotopic _ _ (sigma.ι _ a ≫ f) (sigma.ι _ a ≫ g)) :
  homotopic _ _ f g :=
begin
  constructor,
  apply homotopy_coprod,
  intros a,
  exact (h a).some,
end

-- Move this
lemma homotopic_of_quotient_map_eq {X Y : cochain_complex A ℤ}
  (f g : X ⟶ Y) (h : (quotient _ _).map f = (quotient _ _).map g) :
  homotopic _ _ f g :=
begin
  erw quotient.functor_map_eq_iff at h, assumption,
end

noncomputable
def colimit_cofan {α : Type v} (X : α → homotopy_category A (complex_shape.up ℤ)) :
  cofan X :=
cofan.mk
((quotient _ _).obj $ sigma_obj (λ a, (X a).as))
(λ a, (quotient _ _).map $ sigma.ι _ a)

noncomputable
def is_colimit_cofan {α : Type v} (X : α → homotopy_category A (complex_shape.up ℤ)) :
  is_colimit (colimit_cofan X) :=
{ desc := λ S, (quotient _ _).map $ sigma.desc $ λ a, (S.ι.app a).out,
  fac' := begin
    intros S j,
    dsimp,
    erw [← (quotient A (complex_shape.up ℤ)).map_comp, colimit.ι_desc],
    dsimp [quotient],
    simp,
  end,
  uniq' := begin
    intros S m hm,
    let mm := m.out,
    have : (quotient _ _).map mm = m, by simp,
    rw ← this,
    apply quot.sound,
    apply quotient.comp_closure.of,
    apply homotopic_coprod,
    intros a,
    specialize hm a, rw ← this at hm, dsimp at hm,
    erw [← (quotient A (complex_shape.up ℤ)).map_comp] at hm,
    erw colimit.ι_desc,
    dsimp,
    have : S.ι.app a = (quotient _ _).map (S.ι.app a).out, by simp,
    rw this at hm,
    apply homotopic_of_quotient_map_eq,
    exact hm
  end }

instance {α : Type v} (X : α → homotopy_category A (complex_shape.up ℤ)) :
  has_coproduct X :=
{ exists_colimit := nonempty.intro $ ⟨colimit_cofan _, is_colimit_cofan _⟩ }

instance {α : Type v} : has_colimits_of_shape (discrete α)
  (homotopy_category A (complex_shape.up ℤ)) :=
begin
  constructor, intros K,
  let E : K ≅ discrete.functor K.obj := discrete.nat_iso (λ _, iso.refl _),
  apply has_colimit_of_iso E,
end

noncomputable
instance {α : Type v} : preserves_colimits_of_shape (discrete α)
  (quotient A (complex_shape.up ℤ)) :=
begin
  constructor, intros K,
  apply preserves_colimit_of_preserves_colimit_cocone
    (colimit.is_colimit K),
  let T : K ⋙ quotient A _ ≅ discrete.functor
    ((λ a : α, (quotient _ _).obj (K.obj a))) := nat_iso.of_components
    (λ _, iso.refl _) _,
  swap,
  { rintros i _ ⟨⟨⟨⟩⟩⟩, dsimp, simpa },
  apply (is_colimit.precompose_inv_equiv T
    ((quotient A (complex_shape.up ℤ)).map_cocone (colimit.cocone K))).to_fun,
  let ee : colimit_cofan (λ a : α, (quotient _ _).obj (K.obj a)) ≅
    (cocones.precompose T.inv).obj
    ((quotient A (complex_shape.up ℤ)).map_cocone (colimit.cocone K)) := _,
  swap,
  { refine cocones.ext _ _,
    { apply functor.map_iso,
      refine has_colimit.iso_of_nat_iso _,
      refine nat_iso.of_components (λ _, iso.refl _) _,
      rintro i _ ⟨⟨⟨⟩⟩⟩, dsimp, simpa },
    intros i,
    dsimp [colimit_cofan, T, nat_iso.of_components,
      has_colimit.iso_of_nat_iso, is_colimit.map],
    simp only [← functor.map_comp, category.id_comp, colimit.ι_desc],
    dsimp [cocones.precompose],
    simp only [category.id_comp] },
  apply is_colimit.of_iso_colimit _ ee,
  apply is_colimit_cofan,
end

instance is_K_projective_sigma {α : Type v}
  (X : α → homotopy_category A (complex_shape.up ℤ))
  [∀ a, is_K_projective (X a)] : is_K_projective (sigma_obj X) :=
begin
  constructor,
  introsI Y hY f,
  apply colimit.hom_ext,
  intros a,
  rw comp_zero,
  apply is_K_projective.cond Y,
  dsimp, apply_instance,
end

instance is_K_projective_colimit_cofan {α : Type v}
  (X : α → homotopy_category A (complex_shape.up ℤ))
  [∀ a, is_K_projective (X a)] : is_K_projective (colimit_cofan X).X :=
begin
  let e : (colimit_cofan X).X ≅ sigma_obj X :=
    (is_colimit_cofan X).cocone_point_unique_up_to_iso (colimit.is_colimit _),
  apply is_K_projective_of_iso _ _ e.symm,
end

end homotopy_category

author: bentoner

repo: debug

save_path: github-repos/lean/bentoner-debug


text:
import ..dual

open_locale classical

open set list

namespace matroid

variables {E : Type*} [finite E] {X Y I C B F : set E} {N M : matroid E} {e f : E}

section weak_image
/- `M` is a weak image of `N` if independence in `N` implies independence in `M` -/
def weak_image (N M : matroid E) :=
  ∀ I, N.indep I → M.indep I

-- instance weak_image_le : has_le (matroid E) :=
-- ⟨λ N M, is_weak_image N M⟩

reserve infixl ` ≤w `:75
infix ` ≤w ` := weak_image

lemma weak_image_def :
  N ≤w M ↔ ∀ I, N.indep I → M.indep I :=
iff.rfl

lemma indep.weak_image (hI : N.indep I) (h : N ≤w M)  :
  M.indep I :=
h _ hI

lemma weak_image_iff_r:
  N ≤w M ↔ ∀ X, N.r X ≤ M.r X :=
begin
  simp_rw [r_le_iff, le_r_iff],
  refine ⟨λ h X I hIN hIX, ⟨I,h _ hIN, hIX, rfl⟩, λ h I hI, _⟩,
  obtain ⟨J,hJ,hJI,hJ'⟩ := h I I hI subset.rfl,
  rwa [←eq_of_subset_of_ncard_le hJI hJ'.symm.le],
end

lemma weak_image.r_le (h : N ≤w M) (X : set E) :
  N.r X ≤ M.r X :=
weak_image_iff_r.mp h X

lemma weak_image_iff_dep:
  N ≤w M ↔ ∀ X, ¬M.indep X → ¬N.indep X :=
by simp_rw [weak_image_def, not_imp_not]

lemma weak_image.dep (h : N ≤w M) (hX : ¬M.indep X) :
  ¬ N.indep X :=
weak_image_iff_dep.mp h _ hX

lemma weak_image_iff_circuit:
  N ≤w M ↔ ∀ C, M.circuit C → ∃ C' ⊆ C, N.circuit C' :=
begin
  simp_rw [weak_image_iff_dep, dep_iff_supset_circuit],
  refine ⟨λ h, λ C hC, _, λ h, λ X hX, _⟩,
  {  apply h, exact ⟨C,subset_refl _, hC⟩,},
  rcases hX with ⟨C, ⟨h', h''⟩⟩,
  rcases h C h'' with ⟨C',h1,h2⟩,
  refine ⟨C', h1.trans h', h2⟩,
end

lemma circuit.supset_circuit_of_weak_image (hC : M.circuit C) (h : N ≤w M) :
  ∃ C' ⊆ C, N.circuit C' :=
weak_image_iff_circuit.mp h _ hC

lemma weak_image_tfae:
  tfae
[ N ≤w M,
  ∀ X, N.r X ≤ M.r X,
  ∀ X, N.indep X → M.indep X,
  ∀ X, ¬M.indep X → ¬N.indep X,
  ∀ C, M.circuit C → ∃ C' ⊆ C, N.circuit C'] :=
begin
  tfae_have : 1 ↔ 2, apply weak_image_iff_r,
  tfae_have : 1 ↔ 3, apply weak_image_def,
  tfae_have : 1 ↔ 4, apply weak_image_iff_dep,
  tfae_have : 1 ↔ 5, apply weak_image_iff_circuit,
  tfae_finish,
end

lemma weak_image.rank_zero_of_rank_zero (h : N ≤w M) (hX : M.r X = 0) :
  N.r X = 0 :=
nat.eq_zero_of_le_zero ((weak_image.r_le h X).trans_eq hX)

lemma loop.weak_image (he : M.loop e) (h : N ≤w M) :
  N.loop e :=
begin
  obtain ⟨C,hCe,hC⟩ :=  he.circuit.supset_circuit_of_weak_image h,
  rw [loop_def],
  convert hC,
  by_contra h',
  rw ssubset_singleton_iff.mp (hCe.ssubset_of_ne (ne.symm h')) at hC,
  simpa using hC.nonempty,
end

lemma nonloop_of_weak_image_nonloop (h : N ≤w M) {e : E} (he : ¬ N.loop e) :
  ¬ M.loop e :=
λ he', he (he'.weak_image h)

lemma weak_image.trans {M₀ M₁ M₂ : matroid E} (h₀₁ : M₀ ≤w M₁) (h₁₂ : M₁ ≤w M₂) :
  M₀ ≤w M₂ :=
λ I hI, h₁₂ I (h₀₁ I hI)

lemma weak_image.antisymm (h : M ≤w N) (h' : N ≤w M) :
  M = N :=
eq_of_indep_iff_indep_forall (λ I, ⟨λ hI, h I hI, λ hI, h' I hI⟩)

end weak_image

section quotient
/-- a quotient of M is a matroid N for which rank differences of nested pairs in N are at most
the corresponding rank differences in M. This is equivalent to the existence of a matroid P for
which M is a deletion of P and N is a contraction of P, but we do not show this equivalence here.
-/
def is_quotient (N M : matroid E) :=
  ∀ X, M.cl X ⊆ N.cl X

reserve infixl ` ≼ `:75
infix ` ≼ ` :=  is_quotient

lemma is_quotient.cl_subset (h : N ≼ M) (X : set E) :
  M.cl X ⊆ N.cl X :=
h X

lemma is_quotient.r_le_r_of_subset (h : N ≼ M) (hXY : X ⊆ Y) :
  (N.r Y : ℤ)  - N.r X ≤ M.r Y - M.r X :=
begin
  by_contra' hlt,
  set P : set E → Prop := λ Z, X ⊆ Z ∧ Z ⊆ Y ∧ (M.r Y : ℤ) - M.r Z < N.r Y - N.r Z,
  obtain ⟨Z,⟨hXZ,hZY,hlt'⟩,hmax⟩ := finite.exists_maximal P ⟨X, subset.rfl, hXY, hlt⟩,
  have hss := hZY.ssubset_of_ne (by {rintro rfl, simpa using hlt'}),
  rw [int.lt_iff_add_one_le, ←le_sub_iff_add_le] at hlt',
  obtain ⟨e,heY,heZ⟩ := exists_of_ssubset hss,

  refine (insert_ne_self.mpr (heZ)).symm
      (hmax (insert e Z) ⟨hXZ.trans (set.subset_insert _ _),
      insert_subset.mpr ⟨heY,hZY⟩, lt_of_not_le (λ hle, _)⟩ (subset_insert _ _)),

  by_cases h₁ : e ∈ M.cl Z,
  { rw [mem_cl.mp h₁, mem_cl.mp (h Z h₁)] at hle,  linarith},

  rw [not_mem_cl.mp h₁, nat.cast_add, nat.cast_one] at hle,
  linarith [N.r_insert_le_add_one Z e],
end

lemma is_quotient_iff_r :
  N ≼ M ↔ ∀ X Y, X ⊆ Y → (N.r Y : ℤ)  - N.r X ≤ M.r Y - M.r X :=
begin
  refine ⟨λ h X Y hXY, h.r_le_r_of_subset hXY, λ h Z e he, _⟩,
  have hle := h _ _ (subset_insert e Z),
  rw [mem_cl.mp he, sub_self, sub_le_iff_le_add, zero_add, nat.cast_le] at hle,
  apply mem_cl_of_r_insert_le hle,
end

lemma is_quotient.weak_image (h : N ≼ M) :
   N ≤w M :=
begin
  refine λ X hX, by_contra (λ h', _),
  obtain ⟨C,hCX,hC⟩ := dep_iff_supset_circuit.mp h',
  obtain ⟨e,heC⟩ := hC.nonempty,
  have he := (hC.subset_cl_diff_singleton e).trans (h (C \ {e})),
  exact ((cl_subset_cl_of_subset_cl he).trans_ssubset
    ((hX.subset hCX).cl_diff_singleton_ssubset heC)).ne rfl,
end

lemma indep.quotient (hI : N.indep I) (h : N ≼ M) :
  M.indep I :=
hI.weak_image h.weak_image

/- TODO : prove without rank (or with relative rank)-/
lemma quotient_iff_dual_quotient :
  N ≼ M ↔ M.dual ≼ N.dual :=
begin
  suffices h' : ∀ (N M : matroid E), N ≼ M → M.dual ≼ N.dual,
  exact ⟨λ h, h' _ _ h, λ h, by {convert h' _ _ h; rw dual_dual, }⟩,
  simp_rw [is_quotient_iff_r, dual_rank_cast_eq],
  intros N M h X Y hXY,
  have := h _ _ (compl_subset_compl.mpr hXY),
  linarith,
end

lemma is_quotient_iff_flat :
  N ≼ M ↔ ∀ F, N.flat F → M.flat F :=
begin
  rw [is_quotient],
  refine ⟨λ h F hNF, _, λ h, _⟩,
  { refine flat_iff_cl_self.mpr ((M.subset_cl _).antisymm' _),
    have hcl := h F, rwa hNF.cl at hcl},
  simp_rw [N.cl_def, subset_sInter_iff, mem_set_of_eq, and_imp],
  exact λ X F hF hXF, (h _ hF).cl_subset_of_subset hXF,
end

lemma flat.quotient (hF : N.flat F) (h : N ≼ M) :
  M.flat F :=
(is_quotient_iff_flat.mp h) F hF

lemma quotient_tfae :
  tfae
[N ≼ M,
 ∀ F, N.flat F → M.flat F,
 ∀ X Y, X ⊆ Y → (N.r Y : ℤ)  - N.r X ≤ M.r Y - M.r X,
 ∀ X, M.cl X ⊆ N.cl X,
 M.dual ≼ N.dual] :=
begin
  tfae_have : 1 ↔ 3, exact is_quotient_iff_r,
  tfae_have : 1 ↔ 2, exact is_quotient_iff_flat,
  tfae_have : 1 ↔ 4, refl,
  tfae_have : 1 ↔ 5, exact quotient_iff_dual_quotient,
  tfae_finish,
end

lemma quotient_iff_cl :
  N ≼ M ↔ ∀ X, M.cl X ⊆ N.cl X :=
by apply @tfae.out _ quotient_tfae 0 3

lemma eq_of_quotient_of_rk_eq_rk (h : N ≼ M) (hr : N.rk = M.rk) :
  N = M :=
begin
  refine eq_of_r_eq_r_forall _,
  by_contra' h',
  obtain ⟨S, hS, hmax⟩ := finite.exists_maximal _ h',
  apply hS,
  obtain ⟨e,heS⟩ := (ne_univ_iff_exists_not_mem S).mp (by {rintro rfl, exact hS hr}),
  have hi : M.r (insert e S) = N.r (insert e S),
  { by_contra hi,
    exact (ssubset_insert heS).ne (hmax _ (ne.symm hi) (subset_insert _ _)), },
  rw is_quotient_iff_r at h,
  have h1 := h _ _ (subset_insert e S),
  have h2 := h _ _ (empty_subset S),
  rw [hi] at h1,
  simp_rw [r_empty, nat.cast_zero] at h2,
  zify,
  linarith,
end

end quotient

end matroid

repo: lean-matroids


text:
/- Lecture 2.3: Functional Programming — Monads -/

namespace lecture

/- Part 1: Failure is an `option` -/

/- Motivating examples -/

namespace problem

/- Implement `sum_2_5_7 l`: sum up the 2nd, 5th, and 7th elements of list `l`.

How to handle the case when the list has fewer than 7 elements? _Solution:_ Return `option`. -/

def sum_2_5_7_v1 (l : list ℕ) : option ℕ :=
match list.nth l 1 with
| some n2 :=
  match list.nth l 4 with
  | some n5 :=
    match list.nth l 6 with
    | some n7 := some (n2 + n5 + n7)
    | none    := none
    end
  | none    := none
  end
| none    := none
end

def bind {α : Type} {β : Type} : option α → (α → option β) → option β
| none     b := none
| (some a) b := b a

#check λ(f g h : ℕ → ℕ) x, h $ g $ f $ x

def sum_2_5_7_v2 (l : list ℕ) : option ℕ :=
bind (list.nth l 1) $
  λn2, bind (list.nth l 4) $
    λn5, bind (list.nth l 6) $
      λn7, some (n2 + n5 + n7)

#check has_bind.bind -- `do` notation
#check (>>=)

def sum_2_5_7_v3 (l : list ℕ) : option ℕ :=
list.nth l 1 >>=
  λn2, list.nth l 4 >>=
    λn5, list.nth l 6 >>=
      λn7, some (n2 + n5 + n7)

def sum_2_5_7_v4 (l : list ℕ) : option ℕ :=
do
  n2 ← list.nth l 1,
  n5 ← list.nth l 4,
  n7 ← list.nth l 6,
  some (n2 + n5 + n7)

#check @pure

/- The monadic laws for `option` -/

/- `bind` combines two programs. If one of the program is just pure data (`some`), we can remove the bind. -/

/- Pure data as the first program (`some a`):

    do
      a' ← some a,
      f a'
    ═════════════
    f a
-/
lemma option.pure_bind {α β : Type} (a : α) (f : α → option β) :
  some a >>= f = f a :=
by refl
-- this is actually the definition of `option.bind` (i.e. `>>=`)

/- Pure data as the second program (`some a`):

    do
      a ← x,
      some a
    ══════════════
    x
-/
lemma option.bind_pure {α β : Type} : ∀x : option α, x >>= some = x
| none     := by refl
| (some a) := by refl

/- Nested programs `x`, `f`, `g` can be linearized using this associativity rule:

    do
      b ← (do
        a ← x,
        f a),
      g b
    ══════════
    do
      a ← x,
      b ← f a,
      g b
-/
lemma option.bind_assoc {α β γ : Type} {f : α → option β} {g : β → option γ} :
  ∀x : option α, (x >>= f) >>= g = x >>= (λa, f a >>= g)
| none     := by refl
| (some a) := by refl

end problem

/- The monad abstraction -/

class monad (M : Type → Type) extends has_bind M, has_pure M : Type 1 :=
-- law 1: left unit
(pure_bind {α β} (a : α) (f : α → M β) :
  pure a >>= f = f a)
-- law 2: right unit
(bind_pure {α} (m : M α) :
  m >>= pure = m)
-- law 3: associativity
(bind_assoc {α β γ} (f : α → M β) (g : β → M γ) (m : M α) :
  ((m >>= f) >>= g) = (m >>= (λa, f a >>= g)))

attribute [simp] lecture.monad.bind_pure lecture.monad.bind_assoc lecture.monad.pure_bind

open lecture.monad

-- Lean's monads look slightly different, due to separation of syntax and semantics (laws)
#print _root_.monad
#print _root_.is_lawful_monad

/- Part 2: Instances and application -/

/- The option monad: representing failure and partiality -/

namespace option

def pure {α : Type} : α → option α := option.some

def bind {α β : Type} : option α → (α → option β) → option β
| none     f := none
| (some a) f := f a

instance : monad option :=
{ pure       := @option.pure,
  bind       := @option.bind,
  pure_bind  := assume α β a f, by refl,
  bind_pure  := assume α m, match m with none := by refl | some a := by refl end,
  bind_assoc := assume α β γ f g m, match m with none := by refl | some a := by refl end }

end option

/- The state monad: representing an imperative state -/

def state (σ : Type) (α : Type) := σ → α × σ

namespace state

variable {σ : Type}

def get : state σ σ
| s := (s, s)

def set (s : σ) : state σ unit
| t := ((), s)

def bind {α β : Type} (f : state σ α) (g : α → state σ β) : state σ β
| s := function.uncurry g (f s)

def pure {α : Type} (a : α) : state σ α
| s := (a, s)

/- Example: remove all elements which are smaller than a previous elements in the list. -/
def diff_list : list ℕ → state ℕ (list ℕ)
| []       := pure []
| (x :: l) := do
  prev ← get,
  if x < prev then
    do
      diff_list l
  else
    do
      set x,
      l' ← diff_list l,
      pure (x :: l')

/- To execute `diff_list` we need to provide a start state, we also get back the last state (i.e. the
largest element) -/
#eval diff_list [1, 2, 3, 2]  0
#eval diff_list [1, 2, 3, 2, 4, 5, 2]  0

instance : monad (state σ) :=
{ pure       := @state.pure σ,
  bind       := @state.bind σ,
  pure_bind  := assume α β a f, funext $ assume s, by refl,
  bind_pure  := assume α m, funext $ assume s,
  begin
    simp [bind],
    cases (m s),
    refl
  end,
  bind_assoc := assume α β γ f g m, funext $ assume s,
  begin
    simp [bind],
    cases (m s),
    refl
  end }

end state

/- Concrete monadic programs: adding custom operations -/

namespace interaction_example

section

parameters
  {M : Type → Type}
  [monad M]
  (write : string → M unit)
  (read : M string)

example : M bool := do
  write "Enter a truth value:",
  n ← read,
  if n = "true"
    then do write "true", pure tt
    else do write "false", pure ff

def combine_v1 : M string := do
  write "Part 1:",
  p₁ ← read,
  write "Part 2:",
  p₂ ← read,
  write ("Combined: " ++ p₁ ++ p₂),
  pure (p₁ ++ p₂)

def ask (msg : string) : M string := do
  write msg,
  r ← read,
  pure r

def combine_v2 : M string := do
  p₁ ← ask "Part 1:",
  p₂ ← ask "Part 2:",
  write ("Combined: " ++ p₁ ++ p₂),
  pure (p₁ ++ p₂)

set_option pp.binder_types false

-- Example: show equality between basic monadic programs
example : combine_v2 = combine_v1 :=
by simp [combine_v2, combine_v1, ask]

end

end interaction_example

/- `mmap`: iterating over a list -/

section mmap

variables {M : Type → Type} [monad M] {α β γ δ : Type}

def mmap (f : α → M β) : list α → M (list β)
| []       := pure []
| (a :: l) := do
  b ← f a,
  l' ← mmap l,
  pure (b :: l')

lemma mmap_append (f : α → M β) :
  ∀(l l' : list α),
    mmap f (l ++ l') = do
      xs ← mmap f l,
      ys ← mmap f l',
      pure (xs ++ ys)
| []       l' := by simp [mmap]
| (a :: l) l' := by simp [mmap, mmap_append l l']

/- `nths l n` selects the `(n + 1)`st elements of each list in `l`.
It fails if not all lists are long enough. Intuitively:

    nths [[x00, x01, …],
          [x10, x11, …],
             ⋮    ⋮
          [xN0, xn2, …]] 3 = [x03, x13, …, xN3]

The lists [xI0, xI1, …] may have different length (but they are all finite). -/

def nths {α : Type} (l : list (list α)) (n : ℕ) : option (list α) :=
mmap (λl, list.nth l n) l

end mmap

end lecture

author: KjellZijlemaker


text:
/-
Copyright (c) 2021 Bhavik Mehta. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Bhavik Mehta
-/
import category_theory.limits.shapes.pullbacks
import category_theory.limits.shapes.binary_products
import category_theory.limits.preserves.shapes.pullbacks

/-!
# Relating monomorphisms and epimorphisms to limits and colimits

If `F` preserves (resp. reflects) pullbacks, then it preserves (resp. reflects) monomorphisms.

## TODO

Dualise and apply to functor categories.

-/

universes v u₁ u₂

namespace category_theory
open category limits

variables {C : Type u₁} {D : Type u₂} [category.{v} C] [category.{v} D]
variables (F : C ⥤ D)

/-- If `F` preserves pullbacks, then it preserves monomorphisms. -/
instance preserves_mono {X Y : C} (f : X ⟶ Y) [preserves_limit (cospan f f) F] [mono f] :
  mono (F.map f) :=
begin
  have := is_limit_pullback_cone_map_of_is_limit F _ (pullback_cone.is_limit_mk_id_id f),
  simp_rw [F.map_id] at this,
  apply pullback_cone.mono_of_is_limit_mk_id_id _ this,
end

/-- If `F` reflects pullbacks, then it reflects monomorphisms. -/
lemma reflects_mono {X Y : C} (f : X ⟶ Y) [reflects_limit (cospan f f) F] [mono (F.map f)] :
  mono f :=
begin
  have := pullback_cone.is_limit_mk_id_id (F.map f),
  simp_rw [←F.map_id] at this,
  apply pullback_cone.mono_of_is_limit_mk_id_id _ (is_limit_of_is_limit_pullback_cone_map F _ this),
end

end category_theory

author: JLimperg


text:
import group_theory.subgroup.basic

universe u

#reduce subgroup.complete_lattice.lt
-- A group is not a union of two proper subgroups
theorem ne_union_of_proper {G : Type u} [group G] (S K : subgroup G) (hS : S < ⊤) (hK : K < ⊤) :
  (S : set G) ∪ K ≠ ⊤ :=
begin
  replace hS := hS.right,
  replace hK := hK.right,
  simp only [subgroup.coe_top, set.subset_def, set.mem_univ, true_implies_iff, not_forall] at hS hK,

  assume hunion,
  simp only [set.ext_iff, set.top_eq_univ, set.mem_univ, set.mem_union, iff_true] at hunion,

  have h1 : ∃ (g : G), g ∈ S ∧ g ∉ K := by {
    apply not_not.mp,
    simp only [not_exists, not_and_distrib, not_not],
    by_contra h,
    have : ∀ (g : G), g ∈ K := λ g,
      or.elim (h g) (λ h, or_iff_not_imp_left.mp (hunion g) h) id,
    exact not_forall.mpr hK this,
  },
  have h2 : ∃ (g : G), g ∈ K ∧ g ∉ S := by {
    apply not_not.mp,
    simp only [not_exists, not_and_distrib, not_not],
    by_contra h,
    have : ∀ (g : G), g ∈ S := λ g,
      or.elim (h g) (λ h, or_iff_not_imp_right.mp (hunion g) h) id,
    exact not_forall.mpr hS this
  },

  let x := h1.some * h2.some,
  suffices h3 : x ∉ S ∧ x ∉ K,
  simp_rw ←not_or_distrib at h3,
  exact absurd (hunion x) h3,

  split,
  exact λ h, absurd
    ((mul_mem_cancel_left h1.some_spec.left).mp h)
    h2.some_spec.right,
  exact λ h, absurd
    ((mul_mem_cancel_right h2.some_spec.left).mp h)
    h1.some_spec.right,
end

-- Kenny Lau's super short solution
theorem ne_union_of_proper2 {G : Type u} [group G] (S K : subgroup G) (hS : S < ⊤) (hK : K < ⊤) :
  (S : set G) ∪ K ≠ ⊤ :=
begin
  intro h, simp [set.ext_iff] at h,
  obtain ⟨x, _, hxs⟩ := set_like.exists_of_lt hS,
  obtain ⟨y, _, hyk⟩ := set_like.exists_of_lt hK,
  cases h (x * y) with hs hk,
  { exact hxs ((subgroup.mul_mem_cancel_right S $ (h y).resolve_right hyk).1 hs) },
  { exact hyk ((subgroup.mul_mem_cancel_left K $ (h x).resolve_left hxs).1 hk) }
end

author: greysome

repo: lean-practice


text:
/-
Copyright (c) 2021 Alex Kontorovich, Heather Macbeth. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Alex Kontorovich, Heather Macbeth
-/
import topology.algebra.constructions
import topology.homeomorph
import group_theory.group_action.basic
/-!
# Monoid actions continuous in the second variable

In this file we define class `has_continuous_const_smul`. We say `has_continuous_const_smul Γ T` if
`Γ` acts on `T` and for each `γ`, the map `x ↦ γ • x` is continuous. (This differs from
`has_continuous_smul`, which requires simultaneous continuity in both variables.)

## Main definitions

* `has_continuous_const_smul Γ T` : typeclass saying that the map `x ↦ γ • x` is continuous on `T`;
* `properly_discontinuous_smul`: says that the scalar multiplication `(•) : Γ → T → T`
  is properly discontinuous, that is, for any pair of compact sets `K, L` in `T`, only finitely
  many `γ:Γ` move `K` to have nontrivial intersection with `L`.
* `homeomorph.smul`: scalar multiplication by an element of a group `Γ` acting on `T`
  is a homeomorphism of `T`.

## Main results

* `is_open_map_quotient_mk_mul` : The quotient map by a group action is open.
* `t2_space_of_properly_discontinuous_smul_of_t2_space` : The quotient by a discontinuous group
  action of a locally compact t2 space is t2.

## Tags

Hausdorff, discrete group, properly discontinuous, quotient space

-/

open_locale topological_space pointwise

open filter set

local attribute [instance] mul_action.orbit_rel

/-- Class `has_continuous_const_smul Γ T` says that the scalar multiplication `(•) : Γ → T → T`
is continuous in the second argument. We use the same class for all kinds of multiplicative
actions, including (semi)modules and algebras.
-/
class has_continuous_const_smul (Γ : Type*) (T : Type*) [topological_space T] [has_smul Γ T]
 : Prop :=
(continuous_const_smul : ∀ γ : Γ, continuous (λ x : T, γ • x))

/-- Class `has_continuous_const_vadd Γ T` says that the additive action `(+ᵥ) : Γ → T → T`
is continuous in the second argument. We use the same class for all kinds of additive actions,
including (semi)modules and algebras.
-/
class has_continuous_const_vadd (Γ : Type*) (T : Type*) [topological_space T]
  [has_vadd Γ T] : Prop :=
(continuous_const_vadd : ∀ γ : Γ, continuous (λ x : T, γ +ᵥ x))

attribute [to_additive] has_continuous_const_smul

export has_continuous_const_smul (continuous_const_smul)

export has_continuous_const_vadd (continuous_const_vadd)

variables {M α β : Type*}

section has_smul
variables [topological_space α] [has_smul M α] [has_continuous_const_smul M α]

@[to_additive]
lemma filter.tendsto.const_smul {f : β → α} {l : filter β} {a : α} (hf : tendsto f l (𝓝 a))
  (c : M) :
  tendsto (λ x, c • f x) l (𝓝 (c • a)) :=
((continuous_const_smul _).tendsto _).comp hf

variables [topological_space β] {f : β → M} {g : β → α} {b : β} {s : set β}

@[to_additive]
lemma continuous_within_at.const_smul (hg : continuous_within_at g s b) (c : M) :
  continuous_within_at (λ x, c • g x) s b :=
hg.const_smul c

@[to_additive]
lemma continuous_at.const_smul (hg : continuous_at g b) (c : M) :
  continuous_at (λ x, c • g x) b :=
hg.const_smul c

@[to_additive]
lemma continuous_on.const_smul (hg : continuous_on g s) (c : M) :
  continuous_on (λ x, c • g x) s :=
λ x hx, (hg x hx).const_smul c

@[continuity, to_additive]
lemma continuous.const_smul (hg : continuous g) (c : M) :
  continuous (λ x, c • g x) :=
(continuous_const_smul _).comp hg

/-- If a scalar is central, then its right action is continuous when its left action is. -/
instance has_continuous_const_smul.op [has_smul Mᵐᵒᵖ α] [is_central_scalar M α] :
  has_continuous_const_smul Mᵐᵒᵖ α :=
⟨ mul_opposite.rec $ λ c, by simpa only [op_smul_eq_smul] using continuous_const_smul c ⟩

@[to_additive] instance mul_opposite.has_continuous_const_smul :
  has_continuous_const_smul M αᵐᵒᵖ :=
⟨λ c, mul_opposite.continuous_op.comp $ mul_opposite.continuous_unop.const_smul c⟩

@[to_additive]
instance [has_smul M β] [has_continuous_const_smul M β] :
  has_continuous_const_smul M (α × β) :=
⟨λ _, (continuous_fst.const_smul _).prod_mk (continuous_snd.const_smul _)⟩

@[to_additive]
instance {ι : Type*} {γ : ι → Type*} [∀ i, topological_space (γ i)] [Π i, has_smul M (γ i)]
  [∀ i, has_continuous_const_smul M (γ i)] : has_continuous_const_smul M (Π i, γ i) :=
⟨λ _, continuous_pi $ λ i, (continuous_apply i).const_smul _⟩

end has_smul

section monoid

variables [topological_space α]
variables [monoid M] [mul_action M α] [has_continuous_const_smul M α]

@[to_additive] instance units.has_continuous_const_smul : has_continuous_const_smul Mˣ α :=
{ continuous_const_smul := λ m, (continuous_const_smul (m : M) : _) }

@[to_additive]
lemma smul_closure_subset (c : M) (s : set α) : c • closure s ⊆ closure (c • s) :=
((set.maps_to_image _ _).closure $ continuous_id.const_smul c).image_subset

@[to_additive]
lemma smul_closure_orbit_subset (c : M) (x : α) :
  c • closure (mul_action.orbit M x) ⊆ closure (mul_action.orbit M x) :=
(smul_closure_subset c _).trans $ closure_mono $ mul_action.smul_orbit_subset _ _

end monoid

section group

variables {G : Type*} [topological_space α] [group G] [mul_action G α]
  [has_continuous_const_smul G α]

@[to_additive]
lemma tendsto_const_smul_iff {f : β → α} {l : filter β} {a : α} (c : G) :
  tendsto (λ x, c • f x) l (𝓝 $ c • a) ↔ tendsto f l (𝓝 a) :=
⟨λ h, by simpa only [inv_smul_smul] using h.const_smul c⁻¹,
  λ h, h.const_smul _⟩

variables [topological_space β] {f : β → α} {b : β}  {s : set β}

@[to_additive]
lemma continuous_within_at_const_smul_iff (c : G) :
  continuous_within_at (λ x, c • f x) s b ↔ continuous_within_at f s b :=
tendsto_const_smul_iff c

@[to_additive]
lemma continuous_on_const_smul_iff (c : G) : continuous_on (λ x, c • f x) s ↔ continuous_on f s :=
forall₂_congr $ λ b hb, continuous_within_at_const_smul_iff c

@[to_additive]
lemma continuous_at_const_smul_iff (c : G) :
  continuous_at (λ x, c • f x) b ↔ continuous_at f b :=
tendsto_const_smul_iff c

@[to_additive]
lemma continuous_const_smul_iff (c : G) :
  continuous (λ x, c • f x) ↔ continuous f :=
by simp only [continuous_iff_continuous_at, continuous_at_const_smul_iff]

/-- The homeomorphism given by scalar multiplication by a given element of a group `Γ` acting on
  `T` is a homeomorphism from `T` to itself. -/
@[to_additive] def homeomorph.smul (γ : G) : α ≃ₜ α :=
{ to_equiv := mul_action.to_perm γ,
  continuous_to_fun  := continuous_const_smul γ,
  continuous_inv_fun := continuous_const_smul γ⁻¹ }

/-- The homeomorphism given by affine-addition by an element of an additive group `Γ` acting on
  `T` is a homeomorphism from `T` to itself. -/
add_decl_doc homeomorph.vadd

@[to_additive]
lemma is_open_map_smul (c : G) : is_open_map (λ x : α, c • x) :=
(homeomorph.smul c).is_open_map

@[to_additive] lemma is_open.smul {s : set α} (hs : is_open s) (c : G) : is_open (c • s) :=
is_open_map_smul c s hs

@[to_additive]
lemma is_closed_map_smul (c : G) : is_closed_map (λ x : α, c • x) :=
(homeomorph.smul c).is_closed_map

@[to_additive] lemma is_closed.smul {s : set α} (hs : is_closed s) (c : G) : is_closed (c • s) :=
is_closed_map_smul c s hs

@[to_additive] lemma closure_smul (c : G) (s : set α) : closure (c • s) = c • closure s :=
((homeomorph.smul c).image_closure s).symm

@[to_additive] lemma interior_smul (c : G) (s : set α) : interior (c • s) = c • interior s :=
((homeomorph.smul c).image_interior s).symm

end group

section group_with_zero

variables {G₀ : Type*} [topological_space α] [group_with_zero G₀] [mul_action G₀ α]
  [has_continuous_const_smul G₀ α]

lemma tendsto_const_smul_iff₀ {f : β → α} {l : filter β} {a : α} {c : G₀} (hc : c ≠ 0) :
  tendsto (λ x, c • f x) l (𝓝 $ c • a) ↔ tendsto f l (𝓝 a) :=
tendsto_const_smul_iff (units.mk0 c hc)

variables [topological_space β] {f : β → α} {b : β} {c : G₀} {s : set β}

lemma continuous_within_at_const_smul_iff₀ (hc : c ≠ 0) :
  continuous_within_at (λ x, c • f x) s b ↔ continuous_within_at f s b :=
tendsto_const_smul_iff (units.mk0 c hc)

lemma continuous_on_const_smul_iff₀ (hc : c ≠ 0) :
  continuous_on (λ x, c • f x) s ↔ continuous_on f s :=
continuous_on_const_smul_iff (units.mk0 c hc)

lemma continuous_at_const_smul_iff₀ (hc : c ≠ 0) :
  continuous_at (λ x, c • f x) b ↔ continuous_at f b :=
continuous_at_const_smul_iff (units.mk0 c hc)

lemma continuous_const_smul_iff₀ (hc : c ≠ 0) :
  continuous (λ x, c • f x) ↔ continuous f :=
continuous_const_smul_iff (units.mk0 c hc)

/-- Scalar multiplication by a non-zero element of a group with zero acting on `α` is a
homeomorphism from `α` onto itself. -/
protected def homeomorph.smul_of_ne_zero (c : G₀) (hc : c ≠ 0) : α ≃ₜ α :=
homeomorph.smul (units.mk0 c hc)

lemma is_open_map_smul₀ {c : G₀} (hc : c ≠ 0) : is_open_map (λ x : α, c • x) :=
(homeomorph.smul_of_ne_zero c hc).is_open_map

lemma is_open.smul₀ {c : G₀} {s : set α} (hs : is_open s) (hc : c ≠ 0) : is_open (c • s) :=
is_open_map_smul₀ hc s hs

lemma interior_smul₀ {c : G₀} (hc : c ≠ 0) (s : set α) : interior (c • s) = c • interior s :=
((homeomorph.smul_of_ne_zero c hc).image_interior s).symm

lemma closure_smul₀ {E} [has_zero E] [mul_action_with_zero G₀ E] [topological_space E]
  [t1_space E] [has_continuous_const_smul G₀ E] (c : G₀) (s : set E) :
  closure (c • s) = c • closure s :=
begin
  rcases eq_or_ne c 0 with rfl|hc,
  { rcases eq_empty_or_nonempty s with rfl|hs,
    { simp },
    { rw [zero_smul_set hs, zero_smul_set hs.closure], exact closure_singleton } },
  { exact ((homeomorph.smul_of_ne_zero c hc).image_closure s).symm }
end

/-- `smul` is a closed map in the second argument.

The lemma that `smul` is a closed map in the first argument (for a normed space over a complete
normed field) is `is_closed_map_smul_left` in `analysis.normed_space.finite_dimension`. -/
lemma is_closed_map_smul_of_ne_zero {c : G₀} (hc : c ≠ 0) : is_closed_map (λ x : α, c • x) :=
(homeomorph.smul_of_ne_zero c hc).is_closed_map

lemma is_closed.smul_of_ne_zero {c : G₀} {s : set α} (hs : is_closed s) (hc : c ≠ 0) :
  is_closed (c • s) :=
is_closed_map_smul_of_ne_zero hc s hs

/-- `smul` is a closed map in the second argument.

The lemma that `smul` is a closed map in the first argument (for a normed space over a complete
normed field) is `is_closed_map_smul_left` in `analysis.normed_space.finite_dimension`. -/
lemma is_closed_map_smul₀ {𝕜 M : Type*} [division_ring 𝕜] [add_comm_monoid M] [topological_space M]
  [t1_space M] [module 𝕜 M] [has_continuous_const_smul 𝕜 M] (c : 𝕜) :
  is_closed_map (λ x : M, c • x) :=
begin
  rcases eq_or_ne c 0 with (rfl|hne),
  { simp only [zero_smul], exact is_closed_map_const },
  { exact (homeomorph.smul_of_ne_zero c hne).is_closed_map },
end

lemma is_closed.smul₀ {𝕜 M : Type*} [division_ring 𝕜] [add_comm_monoid M] [topological_space M]
  [t1_space M] [module 𝕜 M] [has_continuous_const_smul 𝕜 M] (c : 𝕜) {s : set M} (hs : is_closed s) :
  is_closed (c • s) :=
is_closed_map_smul₀ c s hs

end group_with_zero

namespace is_unit

variables [monoid M] [topological_space α] [mul_action M α] [has_continuous_const_smul M α]

lemma tendsto_const_smul_iff {f : β → α} {l : filter β} {a : α} {c : M} (hc : is_unit c) :
  tendsto (λ x, c • f x) l (𝓝 $ c • a) ↔ tendsto f l (𝓝 a) :=
let ⟨u, hu⟩ := hc in hu ▸ tendsto_const_smul_iff u

variables [topological_space β] {f : β → α} {b : β} {c : M} {s : set β}

lemma continuous_within_at_const_smul_iff (hc : is_unit c) :
  continuous_within_at (λ x, c • f x) s b ↔ continuous_within_at f s b :=
let ⟨u, hu⟩ := hc in hu ▸ continuous_within_at_const_smul_iff u

lemma continuous_on_const_smul_iff (hc : is_unit c) :
  continuous_on (λ x, c • f x) s ↔ continuous_on f s :=
let ⟨u, hu⟩ := hc in hu ▸ continuous_on_const_smul_iff u

lemma continuous_at_const_smul_iff (hc : is_unit c) :
  continuous_at (λ x, c • f x) b ↔ continuous_at f b :=
let ⟨u, hu⟩ := hc in hu ▸ continuous_at_const_smul_iff u

lemma continuous_const_smul_iff (hc : is_unit c) :
  continuous (λ x, c • f x) ↔ continuous f :=
let ⟨u, hu⟩ := hc in hu ▸ continuous_const_smul_iff u

lemma is_open_map_smul (hc : is_unit c) : is_open_map (λ x : α, c • x) :=
let ⟨u, hu⟩ := hc in hu ▸ is_open_map_smul u

lemma is_closed_map_smul (hc : is_unit c) : is_closed_map (λ x : α, c • x) :=
let ⟨u, hu⟩ := hc in hu ▸ is_closed_map_smul u

end is_unit

/-- Class `properly_discontinuous_smul Γ T` says that the scalar multiplication `(•) : Γ → T → T`
is properly discontinuous, that is, for any pair of compact sets `K, L` in `T`, only finitely many
`γ:Γ` move `K` to have nontrivial intersection with `L`.
-/
class properly_discontinuous_smul (Γ : Type*) (T : Type*) [topological_space T]
  [has_smul Γ T] : Prop :=
(finite_disjoint_inter_image : ∀ {K L : set T}, is_compact K → is_compact L →
  set.finite {γ : Γ | (((•) γ) '' K) ∩ L ≠ ∅ })

/-- Class `properly_discontinuous_vadd Γ T` says that the additive action `(+ᵥ) : Γ → T → T`
is properly discontinuous, that is, for any pair of compact sets `K, L` in `T`, only finitely many
`γ:Γ` move `K` to have nontrivial intersection with `L`.
-/
class properly_discontinuous_vadd (Γ : Type*) (T : Type*) [topological_space T]
  [has_vadd Γ T] : Prop :=
(finite_disjoint_inter_image : ∀ {K L : set T}, is_compact K → is_compact L →
  set.finite {γ : Γ | (((+ᵥ) γ) '' K) ∩ L ≠ ∅ })

attribute [to_additive] properly_discontinuous_smul

variables {Γ : Type*} [group Γ] {T : Type*} [topological_space T] [mul_action Γ T]

/-- A finite group action is always properly discontinuous
-/
@[priority 100, to_additive] instance fintype.properly_discontinuous_smul [fintype Γ] :
  properly_discontinuous_smul Γ T :=
{ finite_disjoint_inter_image := λ _ _ _ _, set.finite.of_fintype _}

export properly_discontinuous_smul (finite_disjoint_inter_image)

export properly_discontinuous_vadd (finite_disjoint_inter_image)

/-- The quotient map by a group action is open. -/
@[to_additive]
lemma is_open_map_quotient_mk_mul [has_continuous_const_smul Γ T] :
  is_open_map (quotient.mk : T → quotient (mul_action.orbit_rel Γ T)) :=
begin
  intros U hU,
  rw [is_open_coinduced, mul_action.quotient_preimage_image_eq_union_mul U],
  exact is_open_Union (λ γ, (homeomorph.smul γ).is_open_map U hU)
end

/-- The quotient by a discontinuous group action of a locally compact t2 space is t2. -/
@[priority 100, to_additive] instance t2_space_of_properly_discontinuous_smul_of_t2_space
  [t2_space T] [locally_compact_space T] [has_continuous_const_smul Γ T]
  [properly_discontinuous_smul Γ T] : t2_space (quotient (mul_action.orbit_rel Γ T)) :=
begin
  set Q := quotient (mul_action.orbit_rel Γ T),
  rw t2_space_iff_nhds,
  let f : T → Q := quotient.mk,
  have f_op : is_open_map f := is_open_map_quotient_mk_mul,
  rintros ⟨x₀⟩ ⟨y₀⟩ (hxy : f x₀ ≠ f y₀),
  show ∃ (U ∈ 𝓝 (f x₀)) (V ∈ 𝓝 (f y₀)), _,
  have hx₀y₀ : x₀ ≠ y₀ := ne_of_apply_ne _ hxy,
  have hγx₀y₀ : ∀ γ : Γ, γ • x₀ ≠ y₀ := not_exists.mp (mt quotient.sound hxy.symm : _),
  obtain ⟨K₀, L₀, K₀_in, L₀_in, hK₀, hL₀, hK₀L₀⟩ := t2_separation_compact_nhds hx₀y₀,
  let bad_Γ_set := {γ : Γ | (((•) γ) '' K₀) ∩ L₀ ≠ ∅ },
  have bad_Γ_finite : bad_Γ_set.finite := finite_disjoint_inter_image hK₀ hL₀,
  choose u v hu hv u_v_disjoint using λ γ, t2_separation_nhds (hγx₀y₀ γ),
  let U₀₀ := ⋂ γ ∈ bad_Γ_set, ((•) γ) ⁻¹' (u γ),
  let U₀ := U₀₀ ∩ K₀,
  let V₀₀ := ⋂ γ ∈ bad_Γ_set, v γ,
  let V₀ := V₀₀ ∩ L₀,
  have U_nhds : f '' U₀ ∈ 𝓝 (f x₀),
  { apply f_op.image_mem_nhds (inter_mem ((bInter_mem bad_Γ_finite).mpr $ λ γ hγ, _) K₀_in),
    exact (continuous_const_smul _).continuous_at (hu γ) },
  have V_nhds : f '' V₀ ∈ 𝓝 (f y₀),
    from f_op.image_mem_nhds (inter_mem ((bInter_mem bad_Γ_finite).mpr $ λ γ hγ, hv γ) L₀_in),
  refine ⟨f '' U₀, U_nhds, f '' V₀, V_nhds, mul_action.disjoint_image_image_iff.2 _⟩,
  rintros x ⟨x_in_U₀₀, x_in_K₀⟩ γ,
  by_cases H : γ ∈ bad_Γ_set,
  { exact λ h, u_v_disjoint γ ⟨mem_Inter₂.mp x_in_U₀₀ γ H, mem_Inter₂.mp h.1 γ H⟩ },
  { rintros ⟨-, h'⟩,
    simp only [image_smul, not_not, mem_set_of_eq, ne.def] at H,
    exact eq_empty_iff_forall_not_mem.mp H (γ • x) ⟨mem_image_of_mem _ x_in_K₀, h'⟩ },
end

section nhds

section mul_action

variables {G₀ : Type*} [group_with_zero G₀] [mul_action G₀ α]
  [topological_space α] [has_continuous_const_smul G₀ α]

/-- Scalar multiplication preserves neighborhoods. -/
lemma set_smul_mem_nhds_smul {c : G₀} {s : set α} {x : α} (hs : s ∈ 𝓝 x) (hc : c ≠ 0) :
  c • s ∈ 𝓝 (c • x : α) :=
begin
  rw mem_nhds_iff at hs ⊢,
  obtain ⟨U, hs', hU, hU'⟩ := hs,
  exact ⟨c • U, set.smul_set_mono hs', hU.smul₀ hc, set.smul_mem_smul_set hU'⟩,
end

lemma set_smul_mem_nhds_smul_iff {c : G₀} {s : set α} {x : α} (hc : c ≠ 0) :
  c • s ∈ 𝓝 (c • x : α) ↔ s ∈ 𝓝 x :=
begin
  refine ⟨λ h, _, λ h, set_smul_mem_nhds_smul h hc⟩,
  rw [←inv_smul_smul₀ hc x, ←inv_smul_smul₀ hc s],
  exact set_smul_mem_nhds_smul h (inv_ne_zero hc),
end

end mul_action

section distrib_mul_action

variables {G₀ : Type*} [group_with_zero G₀] [add_monoid α] [distrib_mul_action G₀ α]
  [topological_space α] [has_continuous_const_smul G₀ α]

lemma set_smul_mem_nhds_zero_iff {s : set α} {c : G₀} (hc : c ≠ 0) :
  c • s ∈ 𝓝 (0 : α) ↔ s ∈ 𝓝 (0 : α) :=
begin
  refine iff.trans _ (set_smul_mem_nhds_smul_iff hc),
  rw smul_zero,
end

end distrib_mul_action

end nhds

author: Parinya-Siri

repo: lean-machine-learning


text:
import tactic -- remove once library_search bug is fixed
import data.nat.prime
import data.nat.modeq
import orbit.random
import data.finsupp
import orbit.orbit_stabilizer
import for_mathlib.finsum

noncomputable theory

open set classical
open function fintype

open_locale classical

namespace action

variables {G : Type*} [group G] {S : Type*}
variables {μ : laction G S}
variables (a b c s: S)
variables (g h : G)

def orbit_rel : setoid S :=
{ r := λ a b, a ∈ orbit μ b,
  iseqv := ⟨begin
   intro a,
   use (1 : G),
   rw μ.map_one,
  end,
  begin
   intros a b h,
   rcases h with ⟨g, rfl⟩,
   use g⁻¹ ,
   rw [μ.map_assoc, mul_left_inv, μ.map_one],
  end,
  begin
   intros a b c ha hb,
   rcases ha with ⟨g1, rfl⟩,
   rcases hb with ⟨g2, rfl⟩,
   use g1*g2,
   rw μ.map_assoc,
  end⟩
    }
#check orbit
--Defining the set of fixed points of the action G on S. They form a subset of S.
@[reducible] def fixed_points (μ : laction G S) : set S:=
{s : S | ∀ g : G, μ.1 g s = s }

#check @fixed_points
--Dependent instance doesn't work
--instance : has_scalar G S := ⟨ λ g s, μ.1 g s ⟩
--#print notation • #exit
local notation g ` • ` s := μ.1 g s

notation g ` •[` μ `] ` s := μ.1 g s
@[simp]lemma mem_fixed_points_iff : s ∈ fixed_points μ ↔ ∀ (g : G) , (g • s) = s := by refl

--Want to show that if s is in the set of fixed points of μ, then the orbit of s contains only s.#check
lemma orbit_eq_singleton {g : G}{s : S} (μ : laction G S) :
(s ∈ fixed_points μ) → orbit μ s = {s} :=
begin
  intro h,
  ext x,
  simp * at *,
end

--Is it worth proving? Should make iff?
lemma singleton_eq_orbit  {s : S} (μ : laction G S) : (orbit μ s = {s}) → s ∈ fixed_points μ :=
begin
  intros h k,
  apply mem_singleton_iff.1 ,
  rw ← mem_singleton_iff at h,
  simp at *,
  apply singleton_eq_singleton_iff.1,
  rw ← h,
  refine ext _,
  intro x, split,
  {intro hx,
    refine singleton_subset_iff.mp _,
    simp at *,
    use k, exact hx},
  {intro hx,
    refine mem_singleton_of_eq _,
    rw h at hx,
    rw mem_singleton_iff at hx,
    rw hx,
    symmetry,
    apply mem_singleton_iff.1,
    rw ← h,
    simp, use k}
end

--localized "notation `∑` binders `, ` r:(scoped:67 f, finset.sum finset.univ f) := r" in big_operators
--localized "notation `∑` binders ` in ` s `, ` r:(scoped:67 f, finset.sum s f) := r" in big_operators
variable [fintype G]
lemma finite_orbit' [fintype G] {a : S} : finite (orbit μ a) :=
begin
  split, split,
    swap,
    { apply finset.image,
      exact λ g, ⟨μ.1 g a, g, rfl⟩,
      exact (univ : set G).to_finset },
    { simp, -- Nonterminating simp! I promise I will fix it!
      rintro x ⟨g, rfl⟩,
      refine ⟨g, rfl⟩ }
end

#check finset.filter

-- temp exit to do one last boring thing
#exit

--set_option pp.implicit true
--If G is a group with card pⁿ, where p is prime and n ≥ 1, S is a finite set acted upon by G,
--then card S cong card fixed points of S mod p.

lemma card_set_congr_card_fixed_points_mod_prime (μ : laction G S)
 [fintype S] [fintype G] (p : ℕ) (hp : p.prime) (n : ℕ) (hn : n ≥ 1) (hG: card G = p^n):
 nat.modeq p (card S) (card (fixed_points μ) ) :=
 begin
  -- we want to show that card (orbit μ s) ∣ p^n for all s : S by orbit-stabilizer
  -- note that since G is finite we have finite orbits
  have claim : ∀ s : S, card( orbit μ s ) ∣ p^n ,
    {intro s, rw ← hG,
    use (card (stabilizer μ s)),
    rw @orbit_stabilizer G _ S _ s μ , congr,
    },
  sorry
 end
--A p-group is a group s.t. all its elements have order a power of p, p prime
--def p_group (g : G) (p : ℕ ) (h : prime p) : sorry
/-OR SHOULD I MAKE IT A CLASS? Using previous definition of group structure-/
#exit
--THERE IS A WHOLE FILE DEDICATED TO CAUCHY THEOREM
theorem cauchy_theorem [group G][fintype G] {p : ℕ} (hp : p.prime) (h : p ∣ (fincard G)):
∃ (S : subgroup G), fincard S = p := sorry
--need to define order of an element

end action

author: ImperialCollegeLondon

repo: group-theory-game


text:
example (y : ℕ) : (λ x : ℕ, 0) y = 0 :=
begin
  refl
end

example (x : ℕ) : x ≤ x :=
begin
  refl
end

author: Ailrun