text:
/-
Copyright (c) 2017 Scott Morrison. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Stephen Morgan, Scott Morrison

! This file was ported from Lean 3 source module category_theory.products.basic
! leanprover-community/mathlib commit 1ead22342e1a078bd44744ace999f85756555d35
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathbin.CategoryTheory.EqToHom
import Mathbin.CategoryTheory.Functor.Const
import Mathbin.Data.Prod.Basic

/-!
# Cartesian products of categories

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

We define the category instance on `C × D` when `C` and `D` are categories.

We define:
* `sectl C Z` : the functor `C ⥤ C × D` given by `X ↦ ⟨X, Z⟩`
* `sectr Z D` : the functor `D ⥤ C × D` given by `Y ↦ ⟨Z, Y⟩`
* `fst`       : the functor `⟨X, Y⟩ ↦ X`
* `snd`       : the functor `⟨X, Y⟩ ↦ Y`
* `swap`      : the functor `C × D ⥤ D × C` given by `⟨X, Y⟩ ↦ ⟨Y, X⟩`
    (and the fact this is an equivalence)

We further define `evaluation : C ⥤ (C ⥤ D) ⥤ D` and `evaluation_uncurried : C × (C ⥤ D) ⥤ D`,
and products of functors and natural transformations, written `F.prod G` and `α.prod β`.
-/

namespace CategoryTheory

-- declare the `v`'s first; see `category_theory.category` for an explanation
universe v₁ v₂ v₃ v₄ u₁ u₂ u₃ u₄

section

variable (C : Type u₁) [Category.{v₁} C] (D : Type u₂) [Category.{v₂} D]

#print CategoryTheory.prod /-
-- the generates simp lemmas like `id_fst` and `comp_snd`
/-- `prod C D` gives the cartesian product of two categories.

See <https://stacks.math.columbia.edu/tag/001K>.
-/
@[simps (config := { notRecursive := [] })]
instance prod : Category.{max v₁ v₂} (C × D)
    where
  Hom X Y := (X.1 ⟶ Y.1) × (X.2 ⟶ Y.2)
  id X := ⟨𝟙 X.1, 𝟙 X.2⟩
  comp _ _ _ f g := (f.1 ≫ g.1, f.2 ≫ g.2)
#align category_theory.prod CategoryTheory.prod
-/

#print CategoryTheory.prod_id /-
/-- Two rfl lemmas that cannot be generated by `@[simps]`. -/
@[simp]
theorem prod_id (X : C) (Y : D) : 𝟙 (X, Y) = (𝟙 X, 𝟙 Y) :=
  rfl
#align category_theory.prod_id CategoryTheory.prod_id
-/

#print CategoryTheory.prod_comp /-
@[simp]
theorem prod_comp {P Q R : C} {S T U : D} (f : (P, S) ⟶ (Q, T)) (g : (Q, T) ⟶ (R, U)) :
    f ≫ g = (f.1 ≫ g.1, f.2 ≫ g.2) :=
  rfl
#align category_theory.prod_comp CategoryTheory.prod_comp
-/

#print CategoryTheory.isIso_prod_iff /-
theorem isIso_prod_iff {P Q : C} {S T : D} {f : (P, S) ⟶ (Q, T)} :
    IsIso f ↔ IsIso f.1 ∧ IsIso f.2 := by
  constructor
  · rintro ⟨g, hfg, hgf⟩
    simp at hfg hgf
    rcases hfg with ⟨hfg₁, hfg₂⟩
    rcases hgf with ⟨hgf₁, hgf₂⟩
    exact ⟨⟨⟨g.1, hfg₁, hgf₁⟩⟩, ⟨⟨g.2, hfg₂, hgf₂⟩⟩⟩
  · rintro ⟨⟨g₁, hfg₁, hgf₁⟩, ⟨g₂, hfg₂, hgf₂⟩⟩
    dsimp at hfg₁ hgf₁ hfg₂ hgf₂
    refine' ⟨⟨(g₁, g₂), _, _⟩⟩ <;> · simp <;> constructor <;> assumption
#align category_theory.is_iso_prod_iff CategoryTheory.isIso_prod_iff
-/

section

variable {C D}

#print CategoryTheory.prod.etaIso /-
/-- The isomorphism between `(X.1, X.2)` and `X`. -/
@[simps]
def prod.etaIso (X : C × D) : (X.1, X.2) ≅ X
    where
  Hom := (𝟙 _, 𝟙 _)
  inv := (𝟙 _, 𝟙 _)
#align category_theory.prod.eta_iso CategoryTheory.prod.etaIso
-/

#print CategoryTheory.Iso.prod /-
/-- Construct an isomorphism in `C × D` out of two isomorphisms in `C` and `D`. -/
@[simps]
def Iso.prod {P Q : C} {S T : D} (f : P ≅ Q) (g : S ≅ T) : (P, S) ≅ (Q, T)
    where
  Hom := (f.Hom, g.Hom)
  inv := (f.inv, g.inv)
#align category_theory.iso.prod CategoryTheory.Iso.prod
-/

end

end

section

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

#print CategoryTheory.uniformProd /-
/-- `prod.category.uniform C D` is an additional instance specialised so both factors have the same
universe levels. This helps typeclass resolution.
-/
instance uniformProd : Category (C × D) :=
  CategoryTheory.prod C D
#align category_theory.uniform_prod CategoryTheory.uniformProd
-/

end

-- Next we define the natural functors into and out of product categories. For now this doesn't
-- address the universal properties.
namespace Prod

#print CategoryTheory.Prod.sectl /-
/-- `sectl C Z` is the functor `C ⥤ C × D` given by `X ↦ (X, Z)`. -/
@[simps]
def sectl (C : Type u₁) [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D] (Z : D) : C ⥤ C × D
    where
  obj X := (X, Z)
  map X Y f := (f, 𝟙 Z)
#align category_theory.prod.sectl CategoryTheory.Prod.sectl
-/

#print CategoryTheory.Prod.sectr /-
/-- `sectr Z D` is the functor `D ⥤ C × D` given by `Y ↦ (Z, Y)` . -/
@[simps]
def sectr {C : Type u₁} [Category.{v₁} C] (Z : C) (D : Type u₂) [Category.{v₂} D] : D ⥤ C × D
    where
  obj X := (Z, X)
  map X Y f := (𝟙 Z, f)
#align category_theory.prod.sectr CategoryTheory.Prod.sectr
-/

variable (C : Type u₁) [Category.{v₁} C] (D : Type u₂) [Category.{v₂} D]

#print CategoryTheory.Prod.fst /-
/-- `fst` is the functor `(X, Y) ↦ X`. -/
@[simps]
def fst : C × D ⥤ C where
  obj X := X.1
  map X Y f := f.1
#align category_theory.prod.fst CategoryTheory.Prod.fst
-/

#print CategoryTheory.Prod.snd /-
/-- `snd` is the functor `(X, Y) ↦ Y`. -/
@[simps]
def snd : C × D ⥤ D where
  obj X := X.2
  map X Y f := f.2
#align category_theory.prod.snd CategoryTheory.Prod.snd
-/

#print CategoryTheory.Prod.swap /-
/-- The functor swapping the factors of a cartesian product of categories, `C × D ⥤ D × C`. -/
@[simps]
def swap : C × D ⥤ D × C where
  obj X := (X.2, X.1)
  map _ _ f := (f.2, f.1)
#align category_theory.prod.swap CategoryTheory.Prod.swap
-/

#print CategoryTheory.Prod.symmetry /-
/-- Swapping the factors of a cartesion product of categories twice is naturally isomorphic
to the identity functor.
-/
@[simps]
def symmetry : swap C D ⋙ swap D C ≅ 𝟭 (C × D)
    where
  Hom := { app := fun X => 𝟙 X }
  inv := { app := fun X => 𝟙 X }
#align category_theory.prod.symmetry CategoryTheory.Prod.symmetry
-/

/- warning: category_theory.prod.braiding -> CategoryTheory.Prod.braiding is a dubious translation:
lean 3 declaration is
  forall (C : Type.{u3}) [_inst_1 : CategoryTheory.Category.{u1, u3} C] (D : Type.{u4}) [_inst_2 : CategoryTheory.Category.{u2, u4} D], CategoryTheory.Equivalence.{max u1 u2, max u2 u1, max u3 u4, max u4 u3} (Prod.{u3, u4} C D) (CategoryTheory.prod.{u1, u2, u3, u4} C _inst_1 D _inst_2) (Prod.{u4, u3} D C) (CategoryTheory.prod.{u2, u1, u4, u3} D _inst_2 C _inst_1)
but is expected to have type
  forall (C : Type.{u3}) [_inst_1 : CategoryTheory.Category.{u1, u3} C] (D : Type.{u4}) [_inst_2 : CategoryTheory.Category.{u2, u4} D], CategoryTheory.Equivalence.{max u1 u2, max u1 u2, max u4 u3, max u3 u4} (Prod.{u3, u4} C D) (Prod.{u4, u3} D C) (CategoryTheory.prod.{u1, u2, u3, u4} C _inst_1 D _inst_2) (CategoryTheory.prod.{u2, u1, u4, u3} D _inst_2 C _inst_1)
Case conversion may be inaccurate. Consider using '#align category_theory.prod.braiding CategoryTheory.Prod.braidingₓ'. -/
/-- The equivalence, given by swapping factors, between `C × D` and `D × C`.
-/
@[simps]
def braiding : C × D ≌ D × C :=
  Equivalence.mk (swap C D) (swap D C) (NatIso.ofComponents (fun X => eqToIso (by simp)) (by tidy))
    (NatIso.ofComponents (fun X => eqToIso (by simp)) (by tidy))
#align category_theory.prod.braiding CategoryTheory.Prod.braiding

#print CategoryTheory.Prod.swapIsEquivalence /-
instance swapIsEquivalence : IsEquivalence (swap C D) :=
  (by infer_instance : IsEquivalence (braiding C D).Functor)
#align category_theory.prod.swap_is_equivalence CategoryTheory.Prod.swapIsEquivalence
-/

end Prod

section

variable (C : Type u₁) [Category.{v₁} C] (D : Type u₂) [Category.{v₂} D]

#print CategoryTheory.evaluation /-
/-- The "evaluation at `X`" functor, such that
`(evaluation.obj X).obj F = F.obj X`,
which is functorial in both `X` and `F`.
-/
@[simps]
def evaluation : C ⥤ (C ⥤ D) ⥤ D
    where
  obj X :=
    { obj := fun F => F.obj X
      map := fun F G α => α.app X }
  map X Y f :=
    { app := fun F => F.map f
      naturality' := fun F G α => Eq.symm (α.naturality f) }
#align category_theory.evaluation CategoryTheory.evaluation
-/

#print CategoryTheory.evaluationUncurried /-
/-- The "evaluation of `F` at `X`" functor,
as a functor `C × (C ⥤ D) ⥤ D`.
-/
@[simps]
def evaluationUncurried : C × (C ⥤ D) ⥤ D
    where
  obj p := p.2.obj p.1
  map x y f := x.2.map f.1 ≫ f.2.app y.1
  map_comp' X Y Z f g := by
    cases g; cases f; cases Z; cases Y; cases X
    simp only [prod_comp, nat_trans.comp_app, functor.map_comp, category.assoc]
    rw [← nat_trans.comp_app, nat_trans.naturality, nat_trans.comp_app, category.assoc,
      nat_trans.naturality]
#align category_theory.evaluation_uncurried CategoryTheory.evaluationUncurried
-/

variable {C}

/- warning: category_theory.functor.const_comp_evaluation_obj -> CategoryTheory.Functor.constCompEvaluationObj is a dubious translation:
lean 3 declaration is
  forall {C : Type.{u3}} [_inst_1 : CategoryTheory.Category.{u1, u3} C] (D : Type.{u4}) [_inst_2 : CategoryTheory.Category.{u2, u4} D] (X : C), CategoryTheory.Iso.{max u4 u2, max u2 u4} (CategoryTheory.Functor.{u2, u2, u4, u4} D _inst_2 D _inst_2) (CategoryTheory.Functor.category.{u2, u2, u4, u4} D _inst_2 D _inst_2) (CategoryTheory.Functor.comp.{u2, max u3 u2, u2, u4, max u1 u2 u3 u4, u4} D _inst_2 (CategoryTheory.Functor.{u1, u2, u3, u4} C _inst_1 D _inst_2) (CategoryTheory.Functor.category.{u1, u2, u3, u4} C _inst_1 D _inst_2) D _inst_2 (CategoryTheory.Functor.const.{u1, u2, u3, u4} C _inst_1 D _inst_2) (CategoryTheory.Functor.obj.{u1, max (max u1 u2 u3 u4) u2, u3, max (max u3 u2) u2 (max u1 u2 u3 u4) u4} C _inst_1 (CategoryTheory.Functor.{max u3 u2, u2, max u1 u2 u3 u4, u4} (CategoryTheory.Functor.{u1, u2, u3, u4} C _inst_1 D _inst_2) (CategoryTheory.Functor.category.{u1, u2, u3, u4} C _inst_1 D _inst_2) D _inst_2) (CategoryTheory.Functor.category.{max u3 u2, u2, max u1 u2 u3 u4, u4} (CategoryTheory.Functor.{u1, u2, u3, u4} C _inst_1 D _inst_2) (CategoryTheory.Functor.category.{u1, u2, u3, u4} C _inst_1 D _inst_2) D _inst_2) (CategoryTheory.evaluation.{u1, u2, u3, u4} C _inst_1 D _inst_2) X)) (CategoryTheory.Functor.id.{u2, u4} D _inst_2)
but is expected to have type
  forall {C : Type.{u3}} [_inst_1 : CategoryTheory.Category.{u1, u3} C] (D : Type.{u4}) [_inst_2 : CategoryTheory.Category.{u2, u4} D] (X : C), CategoryTheory.Iso.{max u4 u2, max u4 u2} (CategoryTheory.Functor.{u2, u2, u4, u4} D _inst_2 D _inst_2) (CategoryTheory.Functor.category.{u2, u2, u4, u4} D _inst_2 D _inst_2) (CategoryTheory.Functor.comp.{u2, max u3 u2, u2, u4, max (max (max u3 u1) u4) u2, u4} D _inst_2 (CategoryTheory.Functor.{u1, u2, u3, u4} C _inst_1 D _inst_2) (CategoryTheory.Functor.category.{u1, u2, u3, u4} C _inst_1 D _inst_2) D _inst_2 (CategoryTheory.Functor.const.{u1, u2, u3, u4} C _inst_1 D _inst_2) (Prefunctor.obj.{succ u1, max (max (max (succ u3) (succ u4)) (succ u1)) (succ u2), u3, max (max (max u3 u4) u1) u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u3} C (CategoryTheory.Category.toCategoryStruct.{u1, u3} C _inst_1)) (CategoryTheory.Functor.{max u3 u2, u2, max (max (max u4 u3) u2) u1, u4} (CategoryTheory.Functor.{u1, u2, u3, u4} C _inst_1 D _inst_2) (CategoryTheory.Functor.category.{u1, u2, u3, u4} C _inst_1 D _inst_2) D _inst_2) (CategoryTheory.CategoryStruct.toQuiver.{max (max (max u3 u4) u1) u2, max (max (max u3 u4) u1) u2} (CategoryTheory.Functor.{max u3 u2, u2, max (max (max u4 u3) u2) u1, u4} (CategoryTheory.Functor.{u1, u2, u3, u4} C _inst_1 D _inst_2) (CategoryTheory.Functor.category.{u1, u2, u3, u4} C _inst_1 D _inst_2) D _inst_2) (CategoryTheory.Category.toCategoryStruct.{max (max (max u3 u4) u1) u2, max (max (max u3 u4) u1) u2} (CategoryTheory.Functor.{max u3 u2, u2, max (max (max u4 u3) u2) u1, u4} (CategoryTheory.Functor.{u1, u2, u3, u4} C _inst_1 D _inst_2) (CategoryTheory.Functor.category.{u1, u2, u3, u4} C _inst_1 D _inst_2) D _inst_2) (CategoryTheory.Functor.category.{max u3 u2, u2, max (max (max u3 u4) u1) u2, u4} (CategoryTheory.Functor.{u1, u2, u3, u4} C _inst_1 D _inst_2) (CategoryTheory.Functor.category.{u1, u2, u3, u4} C _inst_1 D _inst_2) D _inst_2))) (CategoryTheory.Functor.toPrefunctor.{u1, max (max (max u3 u4) u1) u2, u3, max (max (max u3 u4) u1) u2} C _inst_1 (CategoryTheory.Functor.{max u3 u2, u2, max (max (max u4 u3) u2) u1, u4} (CategoryTheory.Functor.{u1, u2, u3, u4} C _inst_1 D _inst_2) (CategoryTheory.Functor.category.{u1, u2, u3, u4} C _inst_1 D _inst_2) D _inst_2) (CategoryTheory.Functor.category.{max u3 u2, u2, max (max (max u3 u4) u1) u2, u4} (CategoryTheory.Functor.{u1, u2, u3, u4} C _inst_1 D _inst_2) (CategoryTheory.Functor.category.{u1, u2, u3, u4} C _inst_1 D _inst_2) D _inst_2) (CategoryTheory.evaluation.{u1, u2, u3, u4} C _inst_1 D _inst_2)) X)) (CategoryTheory.Functor.id.{u2, u4} D _inst_2)
Case conversion may be inaccurate. Consider using '#align category_theory.functor.const_comp_evaluation_obj CategoryTheory.Functor.constCompEvaluationObjₓ'. -/
/-- The constant functor followed by the evalutation functor is just the identity. -/
@[simps]
def Functor.constCompEvaluationObj (X : C) : Functor.const C ⋙ (evaluation C D).obj X ≅ 𝟭 D :=
  NatIso.ofComponents (fun Y => Iso.refl _) fun Y Z f => by simp
#align category_theory.functor.const_comp_evaluation_obj CategoryTheory.Functor.constCompEvaluationObj

end

variable {A : Type u₁} [Category.{v₁} A] {B : Type u₂} [Category.{v₂} B] {C : Type u₃}
  [Category.{v₃} C] {D : Type u₄} [Category.{v₄} D]

namespace Functor

#print CategoryTheory.Functor.prod /-
/-- The cartesian product of two functors. -/
@[simps]
def prod (F : A ⥤ B) (G : C ⥤ D) : A × C ⥤ B × D
    where
  obj X := (F.obj X.1, G.obj X.2)
  map _ _ f := (F.map f.1, G.map f.2)
#align category_theory.functor.prod CategoryTheory.Functor.prod
-/

#print CategoryTheory.Functor.prod' /-
/- Because of limitations in Lean 3's handling of notations, we do not setup a notation `F × G`.
   You can use `F.prod G` as a "poor man's infix", or just write `functor.prod F G`. -/
/-- Similar to `prod`, but both functors start from the same category `A` -/
@[simps]
def prod' (F : A ⥤ B) (G : A ⥤ C) : A ⥤ B × C
    where
  obj a := (F.obj a, G.obj a)
  map x y f := (F.map f, G.map f)
#align category_theory.functor.prod' CategoryTheory.Functor.prod'
-/

#print CategoryTheory.Functor.prod'CompFst /-
/-- The product `F.prod' G` followed by projection on the first component is isomorphic to `F` -/
@[simps]
def prod'CompFst (F : A ⥤ B) (G : A ⥤ C) : F.prod' G ⋙ CategoryTheory.Prod.fst B C ≅ F :=
  NatIso.ofComponents (fun X => Iso.refl _) fun X Y f => by simp
#align category_theory.functor.prod'_comp_fst CategoryTheory.Functor.prod'CompFst
-/

#print CategoryTheory.Functor.prod'CompSnd /-
/-- The product `F.prod' G` followed by projection on the second component is isomorphic to `G` -/
@[simps]
def prod'CompSnd (F : A ⥤ B) (G : A ⥤ C) : F.prod' G ⋙ CategoryTheory.Prod.snd B C ≅ G :=
  NatIso.ofComponents (fun X => Iso.refl _) fun X Y f => by simp
#align category_theory.functor.prod'_comp_snd CategoryTheory.Functor.prod'CompSnd
-/

section

variable (C)

#print CategoryTheory.Functor.diag /-
/-- The diagonal functor. -/
def diag : C ⥤ C × C :=
  (𝟭 C).prod' (𝟭 C)
#align category_theory.functor.diag CategoryTheory.Functor.diag
-/

/- warning: category_theory.functor.diag_obj -> CategoryTheory.Functor.diag_obj is a dubious translation:
lean 3 declaration is
  forall (C : Type.{u2}) [_inst_3 : CategoryTheory.Category.{u1, u2} C] (X : C), Eq.{succ u2} (Prod.{u2, u2} C C) (CategoryTheory.Functor.obj.{u1, u1, u2, u2} C _inst_3 (Prod.{u2, u2} C C) (CategoryTheory.uniformProd.{u1, u2} C _inst_3 C _inst_3) (CategoryTheory.Functor.diag.{u1, u2} C _inst_3) X) (Prod.mk.{u2, u2} C C X X)
but is expected to have type
  forall (C : Type.{u2}) [_inst_3 : CategoryTheory.Category.{u1, u2} C] (X : C), Eq.{succ u2} (Prod.{u2, u2} C C) (Prefunctor.obj.{succ u1, succ u1, u2, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_3)) (Prod.{u2, u2} C C) (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} (Prod.{u2, u2} C C) (CategoryTheory.Category.toCategoryStruct.{u1, u2} (Prod.{u2, u2} C C) (CategoryTheory.uniformProd.{u1, u2} C _inst_3 C _inst_3))) (CategoryTheory.Functor.toPrefunctor.{u1, u1, u2, u2} C _inst_3 (Prod.{u2, u2} C C) (CategoryTheory.uniformProd.{u1, u2} C _inst_3 C _inst_3) (CategoryTheory.Functor.diag.{u1, u2} C _inst_3)) X) (Prod.mk.{u2, u2} C C X X)
Case conversion may be inaccurate. Consider using '#align category_theory.functor.diag_obj CategoryTheory.Functor.diag_objₓ'. -/
@[simp]
theorem diag_obj (X : C) : (diag C).obj X = (X, X) :=
  rfl
#align category_theory.functor.diag_obj CategoryTheory.Functor.diag_obj

/- warning: category_theory.functor.diag_map -> CategoryTheory.Functor.diag_map is a dubious translation:
lean 3 declaration is
  forall (C : Type.{u2}) [_inst_3 : CategoryTheory.Category.{u1, u2} C] {X : C} {Y : C} (f : Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_3)) X Y), Eq.{succ u1} (Quiver.Hom.{succ u1, u2} (Prod.{u2, u2} C C) (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} (Prod.{u2, u2} C C) (CategoryTheory.Category.toCategoryStruct.{u1, u2} (Prod.{u2, u2} C C) (CategoryTheory.uniformProd.{u1, u2} C _inst_3 C _inst_3))) (CategoryTheory.Functor.obj.{u1, u1, u2, u2} C _inst_3 (Prod.{u2, u2} C C) (CategoryTheory.uniformProd.{u1, u2} C _inst_3 C _inst_3) (CategoryTheory.Functor.diag.{u1, u2} C _inst_3) X) (CategoryTheory.Functor.obj.{u1, u1, u2, u2} C _inst_3 (Prod.{u2, u2} C C) (CategoryTheory.uniformProd.{u1, u2} C _inst_3 C _inst_3) (CategoryTheory.Functor.diag.{u1, u2} C _inst_3) Y)) (CategoryTheory.Functor.map.{u1, u1, u2, u2} C _inst_3 (Prod.{u2, u2} C C) (CategoryTheory.uniformProd.{u1, u2} C _inst_3 C _inst_3) (CategoryTheory.Functor.diag.{u1, u2} C _inst_3) X Y f) (Prod.mk.{u1, u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_3)) (Prod.fst.{u2, u2} C C (CategoryTheory.Functor.obj.{u1, u1, u2, u2} C _inst_3 (Prod.{u2, u2} C C) (CategoryTheory.uniformProd.{u1, u2} C _inst_3 C _inst_3) (CategoryTheory.Functor.diag.{u1, u2} C _inst_3) X)) (Prod.fst.{u2, u2} C C (CategoryTheory.Functor.obj.{u1, u1, u2, u2} C _inst_3 (Prod.{u2, u2} C C) (CategoryTheory.uniformProd.{u1, u2} C _inst_3 C _inst_3) (CategoryTheory.Functor.diag.{u1, u2} C _inst_3) Y))) (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_3)) (Prod.snd.{u2, u2} C C (CategoryTheory.Functor.obj.{u1, u1, u2, u2} C _inst_3 (Prod.{u2, u2} C C) (CategoryTheory.uniformProd.{u1, u2} C _inst_3 C _inst_3) (CategoryTheory.Functor.diag.{u1, u2} C _inst_3) X)) (Prod.snd.{u2, u2} C C (CategoryTheory.Functor.obj.{u1, u1, u2, u2} C _inst_3 (Prod.{u2, u2} C C) (CategoryTheory.uniformProd.{u1, u2} C _inst_3 C _inst_3) (CategoryTheory.Functor.diag.{u1, u2} C _inst_3) Y))) f f)
but is expected to have type
  forall (C : Type.{u2}) [_inst_3 : CategoryTheory.Category.{u1, u2} C] {X : C} {Y : C} (f : Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_3)) X Y), Eq.{succ u1} (Quiver.Hom.{succ u1, u2} (Prod.{u2, u2} C C) (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} (Prod.{u2, u2} C C) (CategoryTheory.Category.toCategoryStruct.{u1, u2} (Prod.{u2, u2} C C) (CategoryTheory.uniformProd.{u1, u2} C _inst_3 C _inst_3))) (Prefunctor.obj.{succ u1, succ u1, u2, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_3)) (Prod.{u2, u2} C C) (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} (Prod.{u2, u2} C C) (CategoryTheory.Category.toCategoryStruct.{u1, u2} (Prod.{u2, u2} C C) (CategoryTheory.uniformProd.{u1, u2} C _inst_3 C _inst_3))) (CategoryTheory.Functor.toPrefunctor.{u1, u1, u2, u2} C _inst_3 (Prod.{u2, u2} C C) (CategoryTheory.uniformProd.{u1, u2} C _inst_3 C _inst_3) (CategoryTheory.Functor.diag.{u1, u2} C _inst_3)) X) (Prefunctor.obj.{succ u1, succ u1, u2, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_3)) (Prod.{u2, u2} C C) (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} (Prod.{u2, u2} C C) (CategoryTheory.Category.toCategoryStruct.{u1, u2} (Prod.{u2, u2} C C) (CategoryTheory.uniformProd.{u1, u2} C _inst_3 C _inst_3))) (CategoryTheory.Functor.toPrefunctor.{u1, u1, u2, u2} C _inst_3 (Prod.{u2, u2} C C) (CategoryTheory.uniformProd.{u1, u2} C _inst_3 C _inst_3) (CategoryTheory.Functor.diag.{u1, u2} C _inst_3)) Y)) (Prefunctor.map.{succ u1, succ u1, u2, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_3)) (Prod.{u2, u2} C C) (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} (Prod.{u2, u2} C C) (CategoryTheory.Category.toCategoryStruct.{u1, u2} (Prod.{u2, u2} C C) (CategoryTheory.uniformProd.{u1, u2} C _inst_3 C _inst_3))) (CategoryTheory.Functor.toPrefunctor.{u1, u1, u2, u2} C _inst_3 (Prod.{u2, u2} C C) (CategoryTheory.uniformProd.{u1, u2} C _inst_3 C _inst_3) (CategoryTheory.Functor.diag.{u1, u2} C _inst_3)) X Y f) (Prod.mk.{u1, u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_3)) X Y) (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_3)) X Y) f f)
Case conversion may be inaccurate. Consider using '#align category_theory.functor.diag_map CategoryTheory.Functor.diag_mapₓ'. -/
@[simp]
theorem diag_map {X Y : C} (f : X ⟶ Y) : (diag C).map f = (f, f) :=
  rfl
#align category_theory.functor.diag_map CategoryTheory.Functor.diag_map

end

end Functor

namespace NatTrans

#print CategoryTheory.NatTrans.prod /-
/-- The cartesian product of two natural transformations. -/
@[simps]
def prod {F G : A ⥤ B} {H I : C ⥤ D} (α : F ⟶ G) (β : H ⟶ I) : F.Prod H ⟶ G.Prod I
    where
  app X := (α.app X.1, β.app X.2)
  naturality' X Y f := by
    cases X; cases Y
    simp only [functor.prod_map, Prod.mk.inj_iff, prod_comp]
    constructor <;> rw [naturality]
#align category_theory.nat_trans.prod CategoryTheory.NatTrans.prod
-/

/- Again, it is inadvisable in Lean 3 to setup a notation `α × β`;
   use instead `α.prod β` or `nat_trans.prod α β`. -/
end NatTrans

/- warning: category_theory.flip_comp_evaluation -> CategoryTheory.flipCompEvaluation is a dubious translation:
lean 3 declaration is
  forall {A : Type.{u4}} [_inst_1 : CategoryTheory.Category.{u1, u4} A] {B : Type.{u5}} [_inst_2 : CategoryTheory.Category.{u2, u5} B] {C : Type.{u6}} [_inst_3 : CategoryTheory.Category.{u3, u6} C] (F : CategoryTheory.Functor.{u1, max u5 u3, u4, max u2 u3 u5 u6} A _inst_1 (CategoryTheory.Functor.{u2, u3, u5, u6} B _inst_2 C _inst_3) (CategoryTheory.Functor.category.{u2, u3, u5, u6} B _inst_2 C _inst_3)) (a : A), CategoryTheory.Iso.{max u5 u3, max u2 u3 u5 u6} (CategoryTheory.Functor.{u2, u3, u5, u6} B _inst_2 C _inst_3) (CategoryTheory.Functor.category.{u2, u3, u5, u6} B _inst_2 C _inst_3) (CategoryTheory.Functor.comp.{u2, max u4 u3, u3, u5, max u1 u3 u4 u6, u6} B _inst_2 (CategoryTheory.Functor.{u1, u3, u4, u6} A _inst_1 C _inst_3) (CategoryTheory.Functor.category.{u1, u3, u4, u6} A _inst_1 C _inst_3) C _inst_3 (CategoryTheory.Functor.flip.{u1, u2, u3, u4, u5, u6} A _inst_1 B _inst_2 C _inst_3 F) (CategoryTheory.Functor.obj.{u1, max (max u1 u3 u4 u6) u3, u4, max (max u4 u3) u3 (max u1 u3 u4 u6) u6} A _inst_1 (CategoryTheory.Functor.{max u4 u3, u3, max u1 u3 u4 u6, u6} (CategoryTheory.Functor.{u1, u3, u4, u6} A _inst_1 C _inst_3) (CategoryTheory.Functor.category.{u1, u3, u4, u6} A _inst_1 C _inst_3) C _inst_3) (CategoryTheory.Functor.category.{max u4 u3, u3, max u1 u3 u4 u6, u6} (CategoryTheory.Functor.{u1, u3, u4, u6} A _inst_1 C _inst_3) (CategoryTheory.Functor.category.{u1, u3, u4, u6} A _inst_1 C _inst_3) C _inst_3) (CategoryTheory.evaluation.{u1, u3, u4, u6} A _inst_1 C _inst_3) a)) (CategoryTheory.Functor.obj.{u1, max u5 u3, u4, max u2 u3 u5 u6} A _inst_1 (CategoryTheory.Functor.{u2, u3, u5, u6} B _inst_2 C _inst_3) (CategoryTheory.Functor.category.{u2, u3, u5, u6} B _inst_2 C _inst_3) F a)
but is expected to have type
  forall {A : Type.{u4}} [_inst_1 : CategoryTheory.Category.{u1, u4} A] {B : Type.{u5}} [_inst_2 : CategoryTheory.Category.{u2, u5} B] {C : Type.{u6}} [_inst_3 : CategoryTheory.Category.{u3, u6} C] (F : CategoryTheory.Functor.{u1, max u5 u3, u4, max (max (max u6 u5) u3) u2} A _inst_1 (CategoryTheory.Functor.{u2, u3, u5, u6} B _inst_2 C _inst_3) (CategoryTheory.Functor.category.{u2, u3, u5, u6} B _inst_2 C _inst_3)) (a : A), CategoryTheory.Iso.{max u5 u3, max (max (max u6 u5) u3) u2} (CategoryTheory.Functor.{u2, u3, u5, u6} B _inst_2 C _inst_3) (CategoryTheory.Functor.category.{u2, u3, u5, u6} B _inst_2 C _inst_3) (CategoryTheory.Functor.comp.{u2, max u4 u3, u3, u5, max (max (max u4 u6) u1) u3, u6} B _inst_2 (CategoryTheory.Functor.{u1, u3, u4, u6} A _inst_1 C _inst_3) (CategoryTheory.Functor.category.{u1, u3, u4, u6} A _inst_1 C _inst_3) C _inst_3 (CategoryTheory.Functor.flip.{u1, u2, u3, u4, u5, u6} A _inst_1 B _inst_2 C _inst_3 F) (Prefunctor.obj.{succ u1, max (max (max (succ u6) (succ u3)) (succ u1)) (succ u4), u4, max (max (max u6 u3) u1) u4} A (CategoryTheory.CategoryStruct.toQuiver.{u1, u4} A (CategoryTheory.Category.toCategoryStruct.{u1, u4} A _inst_1)) (CategoryTheory.Functor.{max u4 u3, u3, max (max (max u6 u4) u3) u1, u6} (CategoryTheory.Functor.{u1, u3, u4, u6} A _inst_1 C _inst_3) (CategoryTheory.Functor.category.{u1, u3, u4, u6} A _inst_1 C _inst_3) C _inst_3) (CategoryTheory.CategoryStruct.toQuiver.{max (max (max u6 u3) u4) u1, max (max (max u6 u3) u4) u1} (CategoryTheory.Functor.{max u4 u3, u3, max (max (max u6 u4) u3) u1, u6} (CategoryTheory.Functor.{u1, u3, u4, u6} A _inst_1 C _inst_3) (CategoryTheory.Functor.category.{u1, u3, u4, u6} A _inst_1 C _inst_3) C _inst_3) (CategoryTheory.Category.toCategoryStruct.{max (max (max u6 u3) u4) u1, max (max (max u6 u3) u4) u1} (CategoryTheory.Functor.{max u4 u3, u3, max (max (max u6 u4) u3) u1, u6} (CategoryTheory.Functor.{u1, u3, u4, u6} A _inst_1 C _inst_3) (CategoryTheory.Functor.category.{u1, u3, u4, u6} A _inst_1 C _inst_3) C _inst_3) (CategoryTheory.Functor.category.{max u4 u3, u3, max (max (max u4 u6) u1) u3, u6} (CategoryTheory.Functor.{u1, u3, u4, u6} A _inst_1 C _inst_3) (CategoryTheory.Functor.category.{u1, u3, u4, u6} A _inst_1 C _inst_3) C _inst_3))) (CategoryTheory.Functor.toPrefunctor.{u1, max (max (max u6 u3) u4) u1, u4, max (max (max u6 u3) u4) u1} A _inst_1 (CategoryTheory.Functor.{max u4 u3, u3, max (max (max u6 u4) u3) u1, u6} (CategoryTheory.Functor.{u1, u3, u4, u6} A _inst_1 C _inst_3) (CategoryTheory.Functor.category.{u1, u3, u4, u6} A _inst_1 C _inst_3) C _inst_3) (CategoryTheory.Functor.category.{max u4 u3, u3, max (max (max u4 u6) u1) u3, u6} (CategoryTheory.Functor.{u1, u3, u4, u6} A _inst_1 C _inst_3) (CategoryTheory.Functor.category.{u1, u3, u4, u6} A _inst_1 C _inst_3) C _inst_3) (CategoryTheory.evaluation.{u1, u3, u4, u6} A _inst_1 C _inst_3)) a)) (Prefunctor.obj.{succ u1, max (succ u5) (succ u3), u4, max (max (max u5 u6) u2) u3} A (CategoryTheory.CategoryStruct.toQuiver.{u1, u4} A (CategoryTheory.Category.toCategoryStruct.{u1, u4} A _inst_1)) (CategoryTheory.Functor.{u2, u3, u5, u6} B _inst_2 C _inst_3) (CategoryTheory.CategoryStruct.toQuiver.{max u5 u3, max (max (max u5 u6) u2) u3} (CategoryTheory.Functor.{u2, u3, u5, u6} B _inst_2 C _inst_3) (CategoryTheory.Category.toCategoryStruct.{max u5 u3, max (max (max u5 u6) u2) u3} (CategoryTheory.Functor.{u2, u3, u5, u6} B _inst_2 C _inst_3) (CategoryTheory.Functor.category.{u2, u3, u5, u6} B _inst_2 C _inst_3))) (CategoryTheory.Functor.toPrefunctor.{u1, max u5 u3, u4, max (max (max u5 u6) u2) u3} A _inst_1 (CategoryTheory.Functor.{u2, u3, u5, u6} B _inst_2 C _inst_3) (CategoryTheory.Functor.category.{u2, u3, u5, u6} B _inst_2 C _inst_3) F) a)
Case conversion may be inaccurate. Consider using '#align category_theory.flip_comp_evaluation CategoryTheory.flipCompEvaluationₓ'. -/
/-- `F.flip` composed with evaluation is the same as evaluating `F`. -/
@[simps]
def flipCompEvaluation (F : A ⥤ B ⥤ C) (a) : F.flip ⋙ (evaluation _ _).obj a ≅ F.obj a :=
  (NatIso.ofComponents fun b => eqToIso rfl) <| by tidy
#align category_theory.flip_comp_evaluation CategoryTheory.flipCompEvaluation

variable (A B C)

#print CategoryTheory.prodFunctorToFunctorProd /-
/-- The forward direction for `functor_prod_functor_equiv` -/
@[simps]
def prodFunctorToFunctorProd : (A ⥤ B) × (A ⥤ C) ⥤ A ⥤ B × C
    where
  obj F := F.1.prod' F.2
  map F G f := { app := fun X => (f.1.app X, f.2.app X) }
#align category_theory.prod_functor_to_functor_prod CategoryTheory.prodFunctorToFunctorProd
-/

#print CategoryTheory.functorProdToProdFunctor /-
/-- The backward direction for `functor_prod_functor_equiv` -/
@[simps]
def functorProdToProdFunctor : (A ⥤ B × C) ⥤ (A ⥤ B) × (A ⥤ C)
    where
  obj F := ⟨F ⋙ CategoryTheory.Prod.fst B C, F ⋙ CategoryTheory.Prod.snd B C⟩
  map F G α :=
    ⟨{  app := fun X => (α.app X).1
        naturality' := fun X Y f => by
          simp only [functor.comp_map, prod.fst_map, ← prod_comp_fst, α.naturality] },
      { app := fun X => (α.app X).2
        naturality' := fun X Y f => by
          simp only [functor.comp_map, prod.snd_map, ← prod_comp_snd, α.naturality] }⟩
#align category_theory.functor_prod_to_prod_functor CategoryTheory.functorProdToProdFunctor
-/

#print CategoryTheory.functorProdFunctorEquivUnitIso /-
/-- The unit isomorphism for `functor_prod_functor_equiv` -/
@[simps]
def functorProdFunctorEquivUnitIso :
    𝟭 _ ≅ prodFunctorToFunctorProd A B C ⋙ functorProdToProdFunctor A B C :=
  NatIso.ofComponents
    (fun F =>
      (((Functor.prod'CompFst _ _).Prod (Functor.prod'CompSnd _ _)).trans (prod.etaIso F)).symm)
    fun F G α => by tidy
#align category_theory.functor_prod_functor_equiv_unit_iso CategoryTheory.functorProdFunctorEquivUnitIso
-/

#print CategoryTheory.functorProdFunctorEquivCounitIso /-
/-- The counit isomorphism for `functor_prod_functor_equiv` -/
@[simps]
def functorProdFunctorEquivCounitIso :
    functorProdToProdFunctor A B C ⋙ prodFunctorToFunctorProd A B C ≅ 𝟭 _ :=
  NatIso.ofComponents (fun F => NatIso.ofComponents (fun X => prod.etaIso (F.obj X)) (by tidy))
    (by tidy)
#align category_theory.functor_prod_functor_equiv_counit_iso CategoryTheory.functorProdFunctorEquivCounitIso
-/

/- warning: category_theory.functor_prod_functor_equiv -> CategoryTheory.functorProdFunctorEquiv is a dubious translation:
lean 3 declaration is
  forall (A : Type.{u4}) [_inst_1 : CategoryTheory.Category.{u1, u4} A] (B : Type.{u5}) [_inst_2 : CategoryTheory.Category.{u2, u5} B] (C : Type.{u6}) [_inst_3 : CategoryTheory.Category.{u3, u6} C], CategoryTheory.Equivalence.{max (max u4 u2) u4 u3, max u4 u2 u3, max (max u1 u2 u4 u5) u1 u3 u4 u6, max u1 (max u2 u3) u4 u5 u6} (Prod.{max u1 u2 u4 u5, max u1 u3 u4 u6} (CategoryTheory.Functor.{u1, u2, u4, u5} A _inst_1 B _inst_2) (CategoryTheory.Functor.{u1, u3, u4, u6} A _inst_1 C _inst_3)) (CategoryTheory.prod.{max u4 u2, max u4 u3, max u1 u2 u4 u5, max u1 u3 u4 u6} (CategoryTheory.Functor.{u1, u2, u4, u5} A _inst_1 B _inst_2) (CategoryTheory.Functor.category.{u1, u2, u4, u5} A _inst_1 B _inst_2) (CategoryTheory.Functor.{u1, u3, u4, u6} A _inst_1 C _inst_3) (CategoryTheory.Functor.category.{u1, u3, u4, u6} A _inst_1 C _inst_3)) (CategoryTheory.Functor.{u1, max u2 u3, u4, max u5 u6} A _inst_1 (Prod.{u5, u6} B C) (CategoryTheory.prod.{u2, u3, u5, u6} B _inst_2 C _inst_3)) (CategoryTheory.Functor.category.{u1, max u2 u3, u4, max u5 u6} A _inst_1 (Prod.{u5, u6} B C) (CategoryTheory.prod.{u2, u3, u5, u6} B _inst_2 C _inst_3))
but is expected to have type
  forall (A : Type.{u4}) [_inst_1 : CategoryTheory.Category.{u1, u4} A] (B : Type.{u5}) [_inst_2 : CategoryTheory.Category.{u2, u5} B] (C : Type.{u6}) [_inst_3 : CategoryTheory.Category.{u3, u6} C], CategoryTheory.Equivalence.{max (max u4 u2) u3, max (max u4 u2) u3, max (max (max (max u6 u4) u3) u1) (max (max u5 u4) u2) u1, max (max (max (max u6 u5) u4) u2 u3) u1} (Prod.{max (max (max u5 u4) u2) u1, max (max (max u6 u4) u3) u1} (CategoryTheory.Functor.{u1, u2, u4, u5} A _inst_1 B _inst_2) (CategoryTheory.Functor.{u1, u3, u4, u6} A _inst_1 C _inst_3)) (CategoryTheory.Functor.{u1, max u2 u3, u4, max u6 u5} A _inst_1 (Prod.{u5, u6} B C) (CategoryTheory.prod.{u2, u3, u5, u6} B _inst_2 C _inst_3)) (CategoryTheory.prod.{max u4 u2, max u4 u3, max (max (max u4 u5) u1) u2, max (max (max u4 u6) u1) u3} (CategoryTheory.Functor.{u1, u2, u4, u5} A _inst_1 B _inst_2) (CategoryTheory.Functor.category.{u1, u2, u4, u5} A _inst_1 B _inst_2) (CategoryTheory.Functor.{u1, u3, u4, u6} A _inst_1 C _inst_3) (CategoryTheory.Functor.category.{u1, u3, u4, u6} A _inst_1 C _inst_3)) (CategoryTheory.Functor.category.{u1, max u2 u3, u4, max u5 u6} A _inst_1 (Prod.{u5, u6} B C) (CategoryTheory.prod.{u2, u3, u5, u6} B _inst_2 C _inst_3))
Case conversion may be inaccurate. Consider using '#align category_theory.functor_prod_functor_equiv CategoryTheory.functorProdFunctorEquivₓ'. -/
/-- The equivalence of categories between `(A ⥤ B) × (A ⥤ C)` and `A ⥤ (B × C)` -/
@[simps]
def functorProdFunctorEquiv : (A ⥤ B) × (A ⥤ C) ≌ A ⥤ B × C
    where
  Functor := prodFunctorToFunctorProd A B C
  inverse := functorProdToProdFunctor A B C
  unitIso := functorProdFunctorEquivUnitIso A B C
  counitIso := functorProdFunctorEquivCounitIso A B C
#align category_theory.functor_prod_functor_equiv CategoryTheory.functorProdFunctorEquiv

end CategoryTheory


text:
/-  Math40001 : Introduction to university mathematics.

Problem Sheet 4, October 2019.

This is a Lean file. It can be read with the Lean theorem prover.

You can work on this file online at
https://tinyurl.com/Lean-M40001-Example-Sheet-4

or you can install Lean and its maths library following the
instructions at
https://github.com/leanprover-community/mathlib#installation

There are advantages to installing Lean on your own computer
(for example it's faster), but it's more hassle than
just using it online.

In the below, delete "sorry" and replace it with some
tactics which prove the result.

-/

import data.real.basic -- the real numbers

/- Question 1.

For each of the sets~$X$ and binary relations~$R$ below, figure out whether~$R$ is (a) reflexive, (b) symmetric, (c) antisymmetric, (d) transitive.

  \begin{enumerate}
  \item Let $X$ be the set $\{1,2\}$ and define~$R$ like this: $R(1,1)$ is true, $R(1,2)$ is true, $R(2,1)$ is true and $R(2,2)$ is false.
  \item Let~$X=\R$ and define $R(a,b)$ to be the proposition $a=-b$.
  \item Let~$X=\R$ and define $R(a,b)$ to be false for all real numbers~$a$ and~$b$.
  \item Let~$X$ be the empty set and define~$R$ to be the empty binary relation (we don't have to say what its value is on any pair $(a,b)$ because no such pairs exist).
  \end{enumerate}

-/

namespace Q1a

inductive X : Type
| one : X
| two : X

namespace X

def R : X → X → Prop
| one one := true
| one two := true
| two one := true
| two two := false

-- insert "¬" if you think it's not reflexive
lemma Q1a_refl : reflexive R :=
begin
  sorry
end

-- insert "¬" if you think it's not symmetric
lemma Q1a_symm : symmetric R :=
begin
  sorry
end

-- insert "¬" if you think it's not transitive
lemma Q1a_trans : transitive R :=
begin
  sorry
end

-- insert "¬" if you think it's not an equiv reln
lemma Q1a_equiv : equivalence R :=
begin
  sorry
end

end X
end Q1a

namespace Q1b

def R (a b : ℝ) : Prop := a = -b

-- insert "¬" if you think it's not reflexive
lemma Q1b_refl : reflexive R :=
begin
  sorry
end

-- insert "¬" if you think it's not symmetric
lemma Q1b_symm : symmetric R :=
begin
  sorry
end

-- insert "¬" if you think it's not transitive
lemma Q1b_trans : transitive R :=
begin
  sorry
end

-- insert "¬" if you think it's not an equiv reln
lemma Q1b_equiv : equivalence R :=
begin
  sorry
end

end Q1b

namespace Q1c

def R (a b : ℝ) : Prop := false

-- insert "¬" if you think it's not reflexive
lemma Q1c_refl : reflexive R :=
begin
  sorry
end

-- insert "¬" if you think it's not symmetric
lemma Q1c_symm : symmetric R :=
begin
  sorry
end

-- insert "¬" if you think it's not transitive
lemma Q1c_trans : transitive R :=
begin
  sorry
end

-- insert "¬" if you think it's not an equiv reln
lemma Q1c_equiv : equivalence R :=
begin
  sorry
end

end Q1c

namespace Q1d

def R (a b : empty) : Prop := by cases a -- i.e. "I'll define it in all cases -- oh look there are no cases"

-- insert "¬" if you think it's not reflexive
lemma Q1d_refl : reflexive R :=
begin
  sorry
end

-- insert "¬" if you think it's not symmetric
lemma Q1d_symm : symmetric R :=
begin
  sorry
end

-- insert "¬" if you think it's not transitive
lemma Q1d_trans : transitive R :=
begin
  sorry
end

-- insert "¬" if you think it's not an equiv reln
lemma Q1d_equiv : equivalence R :=
begin
  sorry
end

end Q1d

-- `set ℤ` is the type of subsets of the integers.

def Q2a : partial_order (set ℤ) :=
{ le := λ A B, A ⊆ B,
  le_refl := begin sorry end,
  le_antisymm := begin sorry end,
  le_trans := begin sorry end
   }

-- insert ¬ at the beginning if you think it's wrong
lemma Q2b : is_total (set ℤ) (λ A B, A ⊆ B) :=
begin
  sorry
end

-- put ¬ in front if you think it's wrong
lemma Q3a : symmetric (λ a b : ℝ, a < b) :=
begin
  sorry
end

-- put ¬ in front if you think it's wrong
lemma Q3b : symmetric (λ a b : (∅ : set ℝ), a < b) :=
begin
  sorry
end

-- type in the proof in the question. Where do you get stuck?
lemma Q4 (X : Type) (R : X → (X → Prop)) (hs : symmetric R) (ht : transitive R) : reflexive R :=
begin
  sorry
end

open function

definition pals {X Y Z : Type} (f : X → Y) (g : X → Z) := ∃ h : Y → Z, bijective h ∧ g = h ∘ f

lemma Q5 (X Y Z: Type) (f : X → Y) (g : X → Z) (hf : surjective f) (hg : surjective g) : pals f g ↔ ∀ a b : X, (f a = f b) ↔ (g a = g b) :=
begin
  sorry
end

author: ImperialCollegeLondon


text:
import affine_algebraic_set.V
import topology.opens
import affine_algebraic_set.V_and_I
import for_mathlib.calle_set

namespace affine_algebraic_set

variables {k : Type*} [integral_domain k] {σ : Type*}

local notation `𝔸ⁿ` := σ → k

open set
open topological_space

instance Zariski_topology  :
  topological_space 𝔸ⁿ :=
{ -- First we need to define what an open is, in lean we need to give a function
  -- from set (n → k) → Prop i.e. a function which takes a set in k^n and
  -- determines if this is open or not.
  is_open := λ U, ∃ (S : set (mv_polynomial σ k)), U = -𝕍 (S),
  -- Secondly we show that univ, the whole set, is open.
  is_open_univ :=
  begin
    -- we know that the whole set will be the required set, so we "use univ"
    use (set.univ : set (mv_polynomial σ k)),
    -- Use fact that V(univ) = ∅
    rw 𝕍_univ,
    -- Putting goal into canonical form, i.e. use the frontend notations such
    -- as - instead of compl
    -- this is important because rewrites wont recognize definitionally
    -- equivalent statements as the same
    show set.univ = - ∅,
    -- Now that we are using canonical form, rewrites will work again.
    -- So we finish up by using fact
    -- that -(∅) = univ
    rw compl_empty,
  end,
  -- Now we show that being open is preserved by intersections.
  is_open_inter :=
  begin
    -- Let U, V be opens and let U_set be the fact that there is some S such
    -- that U = - 𝕍 (S). Similarly for V_set.
    intros U V U_set V_set,
    -- unpack U_set and V_set to access the underlying sets S and T
    cases U_set with S U_comp,
    cases V_set with T V_comp,
    -- Now we wish to show that S*T satisfies the goal
    use S*T,
    -- Use multiplicative property of 𝕍
    rw [𝕍_mul],
    -- TODO: explain convert
    convert (compl_union _ _).symm,
  end,
  -- Finally we wish to show that opens is preserved by arbitary unions
  is_open_sUnion :=
  begin
  -- Let opens be the set of opens that we wish to union over
  intros opens open_comp,
  -- Define H to be the set of sets of polynomials S s.t. - 𝕍 (S) is in opens.
  let H := {S : set (mv_polynomial σ k) | - 𝕍 (S) ∈ opens},
  -- We now want to show that union over H satisfies the goal
  use ⋃₀ H,
  -- converting from sUnion to Union so that we can use the lemma 𝕍_union
  rw @sUnion_eq_Union (mv_polynomial σ k) H,
  rw 𝕍_Union,
  -- putting goal in canonical form
  show ⋃₀ opens = - (⋂ (i : H), 𝕍 (i.val)),
  -- Now that we are using canonical form, rewrites will work again.
  rw compl_Inter,
  rw sUnion_eq_Union,
  -- We prove the two sides are equal by showing the double inclusion
  apply eq_of_subset_of_subset,
    {
      apply Union_subset_Union2,
      intro U,
      cases (open_comp U U.2) with S eq,
      use S,
      change ↑U = compl (𝕍 S) at eq,
        show compl (𝕍 S) ∈ opens, rw ←eq, exact U.2,
      show U.val ⊆ compl (𝕍 (S)),
      rw subset.antisymm_iff at eq,
      cases eq, exact eq_left,
    },
  apply Union_subset_Union2,
  intro S,
  use - 𝕍 S, exact S.2,
  show -𝕍 (S.1) ⊆ -𝕍 (S.1),
  refine set.subset.refl _,
  end
}

open_locale classical

lemma is_closed_iff (C : set 𝔸ⁿ) :
  is_closed C ↔ ∃ (S : set (mv_polynomial σ k)), C = 𝕍 S :=
begin
  unfold is_closed,
  show (∃ (S : set (mv_polynomial σ k)), (compl C) = compl (𝕍 S)) ↔ _,
  rw exists_congr,
  intro S,
  split,
    intro h, ext x, apply not_iff_not.1, rw [←mem_compl_iff, ←mem_compl_iff],
    congr', apply_instance, apply_instance,
  intro h, rw h,
end

theorem zariski_wf {k : Type*} {n : Type*} [fintype n] [integral_domain k] [is_noetherian k k] :
  well_founded ((>) : (opens (n → k) → (opens (n → k)) → Prop)) :=
begin
  have subrel : ∀ (V U: opens (n → k)), U < V → 𝕀' (-↑U) < 𝕀' (-↑V),
    {
      intros U V lt,
      have exists_U_eq_𝕍_S := (is_closed_iff (-↑U)).1 (is_closed_compl_iff.2 U.2),
      cases exists_U_eq_𝕍_S with S U_eq_𝕍_S,
      have exists_V_eq_𝕍_T := (is_closed_iff (-↑V)).1 (is_closed_compl_iff.2 V.2),
      cases exists_V_eq_𝕍_T with T V_eq_𝕍_T,
      rw [U_eq_𝕍_S, V_eq_𝕍_T, submodule.lt_def],
      refine 𝕀_strantimono_on_𝕍 _,
      rw [←U_eq_𝕍_S, ←V_eq_𝕍_T],
      apply compl_lt_compl,
      rw [compl_compl, compl_compl],
      exact lt,
    },
  apply subrelation.wf subrel _,
  refine @inv_image.wf _ _ (>) (λ U : opens (n → k), 𝕀' (-(↑U : set (n → k)))) _,
  apply is_noetherian_iff_well_founded.1,
  refine @is_noetherian_ring_mv_polynomial_of_fintype _ _ _ _ _inst_4,
end

end affine_algebraic_set


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

! This file was ported from Lean 3 source module combinatorics.derangements.basic
! leanprover-community/mathlib commit 9407b03373c8cd201df99d6bc5514fc2db44054f
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Dynamics.FixedPoints.Basic
import Mathlib.GroupTheory.Perm.Option
import Mathlib.Logic.Equiv.Defs
import Mathlib.Logic.Equiv.Option

/-!
# Derangements on types

In this file we define `derangements α`, the set of derangements on a type `α`.

We also define some equivalences involving various subtypes of `Perm α` and `derangements α`:
* `derangementsOptionEquivSigmaAtMostOneFixedPoint`: An equivalence between
  `derangements (Option α)` and the sigma-type `Σ a : α, {f : Perm α // fixed_points f ⊆ a}`.
* `derangementsRecursionEquiv`: An equivalence between `derangements (Option α)` and the
  sigma-type `Σ a : α, (derangements (({a}ᶜ : Set α) : Type _) ⊕ derangements α)` which is later
  used to inductively count the number of derangements.

In order to prove the above, we also prove some results about the effect of `Equiv.removeNone`
on derangements: `RemoveNone.fiber_none` and `RemoveNone.fiber_some`.
-/

open Equiv Function

/-- A permutation is a derangement if it has no fixed points. -/
def derangements (α : Type _) : Set (Perm α) :=
  { f : Perm α | ∀ x : α, f x ≠ x }
#align derangements derangements

variable {α β : Type _}

theorem mem_derangements_iff_fixedPoints_eq_empty {f : Perm α} :
    f ∈ derangements α ↔ fixedPoints f = ∅ :=
  Set.eq_empty_iff_forall_not_mem.symm
#align mem_derangements_iff_fixed_points_eq_empty mem_derangements_iff_fixedPoints_eq_empty

/-- If `α` is equivalent to `β`, then `derangements α` is equivalent to `derangements β`. -/
def Equiv.derangementsCongr (e : α ≃ β) : derangements α ≃ derangements β :=
  e.permCongr.subtypeEquiv fun {f} => e.forall_congr <| by
   intro b; simp only [ne_eq, permCongr_apply, symm_apply_apply, EmbeddingLike.apply_eq_iff_eq]
#align equiv.derangements_congr Equiv.derangementsCongr

namespace derangements

/-- Derangements on a subtype are equivalent to permutations on the original type where points are
fixed iff they are not in the subtype. -/
protected def subtypeEquiv (p : α → Prop) [DecidablePred p] :
    derangements (Subtype p) ≃ { f : Perm α // ∀ a, ¬p a ↔ a ∈ fixedPoints f } :=
  calc
    derangements (Subtype p) ≃
        { f : { f : Perm α // ∀ a, ¬p a → a ∈ fixedPoints f } // ∀ a, a ∈ fixedPoints f → ¬p a } :=
      by
        refine' (Perm.subtypeEquivSubtypePerm p).subtypeEquiv fun f => ⟨fun hf a hfa ha => _, _⟩
        · refine' hf ⟨a, ha⟩ (Subtype.ext _)
          simp_rw [mem_fixedPoints, IsFixedPt, Perm.subtypeEquivSubtypePerm,
          Equiv.coe_fn_mk, Subtype.coe_mk, Perm.ofSubtype_apply_of_mem _ ha] at hfa
          assumption
        rintro hf ⟨a, ha⟩ hfa
        refine' hf _ _ ha
        simp only [Perm.subtypeEquivSubtypePerm_apply_coe, mem_fixedPoints]
        dsimp [IsFixedPt]
        simp_rw [Perm.ofSubtype_apply_of_mem _ ha, hfa]
    _ ≃ { f : Perm α // ∃ _h : ∀ a, ¬p a → a ∈ fixedPoints f, ∀ a, a ∈ fixedPoints f → ¬p a } :=
      subtypeSubtypeEquivSubtypeExists _ _
    _ ≃ { f : Perm α // ∀ a, ¬p a ↔ a ∈ fixedPoints f } :=
      subtypeEquivRight fun f => by
        simp_rw [exists_prop, ← forall_and, ← iff_iff_implies_and_implies]
#align derangements.subtype_equiv derangements.subtypeEquiv

universe u
/-- The set of permutations that fix either `a` or nothing is equivalent to the sum of:
    - derangements on `α`
    - derangements on `α` minus `a`. -/
def atMostOneFixedPointEquivSum_derangements [DecidableEq α] (a : α) :
    { f : Perm α // fixedPoints f ⊆ {a} } ≃ Sum (derangements ({a}ᶜ : Set α)) (derangements α) :=
  calc
    { f : Perm α // fixedPoints f ⊆ {a} } ≃
        Sum { f : { f : Perm α // fixedPoints f ⊆ {a} } // a ∈ fixedPoints f }
          { f : { f : Perm α // fixedPoints f ⊆ {a} } // a ∉ fixedPoints f } :=
      (Equiv.sumCompl _).symm
    _ ≃ Sum { f : Perm α // fixedPoints f ⊆ {a} ∧ a ∈ fixedPoints f }
          { f : Perm α // fixedPoints f ⊆ {a} ∧ a ∉ fixedPoints f } := by
      -- porting note: `subtypeSubtypeEquivSubtypeInter` no longer works with placeholder `_`s.
      refine' Equiv.sumCongr _ _
      . exact subtypeSubtypeEquivSubtypeInter
          (fun x : Perm α => fixedPoints x ⊆ {a})
          (a ∈ fixedPoints ·)
      . exact subtypeSubtypeEquivSubtypeInter
          (fun x : Perm α => fixedPoints x ⊆ {a})
          (¬a ∈ fixedPoints ·)
    _ ≃ Sum { f : Perm α // fixedPoints f = {a} } { f : Perm α // fixedPoints f = ∅ } := by
      refine' Equiv.sumCongr (subtypeEquivRight fun f => _) (subtypeEquivRight fun f => _)
      · rw [Set.eq_singleton_iff_unique_mem, and_comm]
        rfl
      · rw [Set.eq_empty_iff_forall_not_mem]
        refine' ⟨fun h x hx => h.2 (h.1 hx ▸ hx), fun h => ⟨fun x hx => (h _ hx).elim, h _⟩⟩
    _ ≃ Sum (derangements ({a}ᶜ : Set α)) (derangements α) := by
      -- porting note: was `subtypeEquiv _` but now needs the placeholder to be provided explicitly
      refine'
        Equiv.sumCongr ((derangements.subtypeEquiv (· ∈ ({a}ᶜ : Set α))).trans <|
            subtypeEquivRight fun x => _).symm
          (subtypeEquivRight fun f => mem_derangements_iff_fixedPoints_eq_empty.symm)
      rw [eq_comm, Set.ext_iff]
      simp_rw [Set.mem_compl_iff, Classical.not_not]
#align derangements.at_most_one_fixed_point_equiv_sum_derangements derangements.atMostOneFixedPointEquivSum_derangements

namespace Equiv

variable [DecidableEq α]

/-- The set of permutations `f` such that the preimage of `(a, f)` under
    `Equiv.Perm.decomposeOption` is a derangement. -/
def RemoveNone.fiber (a : Option α) : Set (Perm α) :=
  { f : Perm α | (a, f) ∈ Equiv.Perm.decomposeOption '' derangements (Option α) }
#align derangements.equiv.remove_none.fiber derangements.Equiv.RemoveNone.fiber

theorem RemoveNone.mem_fiber (a : Option α) (f : Perm α) :
    f ∈ RemoveNone.fiber a ↔
      ∃ F : Perm (Option α), F ∈ derangements (Option α) ∧ F none = a ∧ removeNone F = f :=
  by simp [RemoveNone.fiber, derangements]
#align derangements.equiv.remove_none.mem_fiber derangements.Equiv.RemoveNone.mem_fiber

theorem RemoveNone.fiber_none : RemoveNone.fiber (@none α) = ∅ := by
  rw [Set.eq_empty_iff_forall_not_mem]
  intro f hyp
  rw [RemoveNone.mem_fiber] at hyp
  rcases hyp with ⟨F, F_derangement, F_none, _⟩
  exact F_derangement none F_none
#align derangements.equiv.remove_none.fiber_none derangements.Equiv.RemoveNone.fiber_none

/-- For any `a : α`, the fiber over `some a` is the set of permutations
    where `a` is the only possible fixed point. -/
theorem RemoveNone.fiber_some (a : α) :
    RemoveNone.fiber (some a) = { f : Perm α | fixedPoints f ⊆ {a} } := by
  ext f
  constructor
  · rw [RemoveNone.mem_fiber]
    rintro ⟨F, F_derangement, F_none, rfl⟩ x x_fixed
    rw [mem_fixedPoints_iff] at x_fixed
    apply_fun some  at x_fixed
    cases' Fx : F (some x) with y
    · rwa [removeNone_none F Fx, F_none, Option.some_inj, eq_comm] at x_fixed
    · exfalso
      rw [removeNone_some F ⟨y, Fx⟩] at x_fixed
      exact F_derangement _ x_fixed
  · intro h_opfp
    use Equiv.Perm.decomposeOption.symm (some a, f)
    constructor
    · intro x
      apply_fun fun x => Equiv.swap none (some a) x
      simp only [Perm.decomposeOption_symm_apply, swap_apply_self, Perm.coe_mul]
      cases' x with x
      · simp
      simp only [comp, optionCongr_apply, Option.map_some', swap_apply_self]
      by_cases x_vs_a : x = a
      · rw [x_vs_a, swap_apply_right]
        apply Option.some_ne_none
      have ne_1 : some x ≠ none := Option.some_ne_none _
      have ne_2 : some x ≠ some a := (Option.some_injective α).ne_iff.mpr x_vs_a
      rw [swap_apply_of_ne_of_ne ne_1 ne_2, (Option.some_injective α).ne_iff]
      intro contra
      exact x_vs_a (h_opfp contra)
    · rw [apply_symm_apply]
#align derangements.equiv.remove_none.fiber_some derangements.Equiv.RemoveNone.fiber_some

end Equiv

section Option

variable [DecidableEq α]

/-- The set of derangements on `Option α` is equivalent to the union over `a : α`
    of "permutations with `a` the only possible fixed point". -/
def derangementsOptionEquivSigmaAtMostOneFixedPoint :
    derangements (Option α) ≃ Σa : α, { f : Perm α | fixedPoints f ⊆ {a} } := by
  have fiber_none_is_false : Equiv.RemoveNone.fiber (@none α) → False :=
    by
    rw [Equiv.RemoveNone.fiber_none]
    exact IsEmpty.false
  calc
    derangements (Option α) ≃ Equiv.Perm.decomposeOption '' derangements (Option α) :=
      Equiv.image _ _
    _ ≃ Σa : Option α, ↥(Equiv.RemoveNone.fiber a) := setProdEquivSigma _
    _ ≃ Σa : α, ↥(Equiv.RemoveNone.fiber (some a)) :=
      sigmaOptionEquivOfSome _ fiber_none_is_false
    _ ≃ Σa : α, { f : Perm α | fixedPoints f ⊆ {a} } := by
      simp_rw [Equiv.RemoveNone.fiber_some]
      rfl
#align derangements.derangements_option_equiv_sigma_at_most_one_fixed_point derangements.derangementsOptionEquivSigmaAtMostOneFixedPoint

/-- The set of derangements on `Option α` is equivalent to the union over all `a : α` of
    "derangements on `α` ⊕ derangements on `{a}ᶜ`". -/
def derangementsRecursionEquiv :
    derangements (Option α) ≃
      Σa : α, Sum (derangements (({a}ᶜ : Set α) : Type _)) (derangements α) :=
  derangementsOptionEquivSigmaAtMostOneFixedPoint.trans
    (sigmaCongrRight atMostOneFixedPointEquivSum_derangements)
#align derangements.derangements_recursion_equiv derangements.derangementsRecursionEquiv

end Option

end derangements

author: leanprover-community


text:
/-
Copyright (c) 2022 Jun Yoshida. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
-/

import Std.Data.Array.Basic
import Std.Data.Array.Lemmas
import Dijkstra.Control.Functor.Subreg

import Algdata.Init.Nat
import Algdata.Init.Fin
import Algdata.Init.GetElem
import Algdata.Data.Array.Lemmas
import Algdata.Data.Array.Modify

universe u v w

@[unbox]
structure Matrix (α : Type u) (r c : Nat) where
  entry : Array α
  hsize : entry.size = r * c

attribute [simp] Matrix.hsize

namespace Matrix

/-!
## Basic operations
-/

section BasicOp

variable {α : Type u} {r c : Nat}

--- Get the `(i,j)`-entry of a given matrix
def get (a : @& Matrix α r c) (i : @& Fin r) (j : @& Fin c) : α :=
  a.entry[a.hsize.symm ▸ Fin.lexFold i j]

--- Substitute a value into the `(i,j)`-entry of a given matrix
def set (a : Matrix α r c) (i : @& Fin r) (j : @& Fin c) (v : α) : Matrix α r c where
  entry := a.entry.set (a.hsize.symm ▸ Fin.lexFold i j) v
  hsize := (Array.size_set a.entry _ v).symm ▸ a.hsize

--- Counterpart of `Array.get_set_eq`
@[simp]
theorem get_set_eq (a : Matrix α r c) (i : Fin r) (j : Fin c) (v : α) : get (a.set i j v) i j = v := by
  dsimp [get, set]
  rw [getElem_eq (by rw [Fin.subst_eq]) (Fin.subst_val _)]
  dsimp [Fin.lexFold]
  rw [Array.get_set_eq a.entry]

--- Counterpart of `Array.get_set_ne` for distinct rwo indices.
theorem get_set_ne_row (a : Matrix α r c) {i₁ i₂ : Fin r} (h : i₁ ≠ i₂) (j : Fin c) (v : α) : get (a.set i₁ j v) i₂ j = get a i₂ j := by
  dsimp [set, get]
  conv => lhs; rw [getElem_eq (by rw [Fin.subst_eq]) (Fin.subst_val _)]
  conv => rhs; rw [getElem_eq rfl (Fin.subst_val _)]
  apply Array.get_set_ne a.entry
  dsimp
  intro hcontra
  have := Fin.lexFold_inj (Fin.eq_of_val_eq hcontra)
  exact absurd this.left h

--- Counterpart of `Array.get_set_ne` for distinct column indices.
theorem get_set_ne_col (a : Matrix α r c) (i : Fin r) {j₁ j₂ : Fin c} (h : j₁ ≠ j₂) (v : α) : get (a.set i j₁ v) i j₂ = get a i j₂ := by
  dsimp [set, get]
  conv => lhs; rw [getElem_eq (by rw [Fin.subst_eq]) (Fin.subst_val _)]
  conv => rhs; rw [getElem_eq rfl (Fin.subst_val _)]
  apply Array.get_set_ne a.entry
  dsimp
  intro hcontra
  have := Fin.lexFold_inj (Fin.eq_of_val_eq hcontra)
  exact absurd this.right h

end BasicOp

/-!
## Construction of matrices
-/

section Construction

variable {α : Type u}

--- Define a matrix whose entries are specified by a function
def ofFn {r c : Nat} (f : Fin r → Fin c → α) : Matrix α r c where
  entry := Array.ofFn (n:=r*c) $ λ k =>
    have : c > 0 := by
      cases Nat.eq_zero_or_pos c
      case inl h =>
        cases h
        cases k with | mk k hk =>
        rw [Nat.mul_zero] at hk
        exact absurd hk (Nat.not_lt_zero k)
      case inr h => exact h
    let i : Fin r := Fin.mk (k / c) ((Nat.div_lt_iff_lt_mul this).mpr k.isLt)
    let j : Fin c := Fin.mk (k % c) (Nat.mod_lt _ this)
    f i j
  hsize := Array.size_ofFn _

--- Constructing the zero matrix with given size
def zero [OfNat α (nat_lit 0)] (r c : Nat) : Matrix α r c where
  entry := Array.mkArray (r*c) 0
  hsize := Array.size_mkArray _ _

--- A square diagonal matrix with given array as diagonal
def diag {α : Type u} [OfNat α (nat_lit 0)] (ds : Array α) : Matrix α ds.size ds.size :=
  Fin.foldAll (n:=ds.size) (λ i x => x.set i i ds[i]) (zero ds.size ds.size)

--- A square diagonal matrix whose diagonal entries are specified by a function
def diagFn {α : Type u} [OfNat α (nat_lit 0)] {n : Nat} (f : Fin n → α) : Matrix α n n :=
  Fin.foldAll (n:=n) (λ i x => x.set i i (f i)) (zero n n)

end Construction

/-!
## modifyM

Apply a (monadic) operation to specific entries of a matrix.

-/

section modifyM

variable {α : Type u} {r c : Nat}

-- cf. modifyMUnsafe in Init.Data.Array.Basic
def modifyM {m : Type _ → Type _} [Monad m] (a : Matrix α r c) (i : Fin r) (j : Fin c) (f : α → m α) : m (Matrix α r c) := do
  let v ← f (a.get i j)
  pure $ a.set i j v

-- use `Array.modifyM` function directly
-- TODO: performance comparison with `modifyM` above
def modifyM' {m : Type _ → Type _} [Monad m] [LawfulMonad m] [SubregFunctor m] (a : Matrix α r c) (i : Fin r) (j : Fin c) (f : α → m α) : m (Matrix α r c) := do
  let w ← SubregFunctor.ensureF _ (a.entry.size_modifyM (i.val*c + j.val) f)
  pure {entry:=w.val, hsize:=by rw[w.property,a.hsize]}

def modify (a : Matrix α r c) (i : Fin r) (j : Fin c) (f : α → α) : Matrix α r c :=
  Id.run <| a.modifyM i j f

def modifyRowM {m : Type _ → Type _} [Monad m] (a : Matrix α r c) (i : Fin r) (f : α → m α) : m (Matrix α r c) :=
  Fin.foldAllM (n:=c) (λ j b => b.modifyM i j f) a

def modifyRow (a : Matrix α r c) (i : Fin r) (f : α → α) : Matrix α r c :=
  Id.run <| a.modifyRowM i f

def modifyColM {m : Type _ → Type _} [Monad m] (a : Matrix α r c) (j : Fin c) (f : α → m α) : m (Matrix α r c) :=
  Fin.foldAllM (n:=r) (λ i b => b.modifyM i j f) a

def modifyCol (a : Matrix α r c) (j : Fin c) (f : α → α) : Matrix α r c :=
  Id.run <| a.modifyColM j f

-- Modification of a row with column indices
def modifyRowIdxM {m : Type _ → Type _} [Monad m] (a : Matrix α r c) (i : Fin r) (f : Fin c → α → m α) : m (Matrix α r c) :=
  Fin.foldAllM (n:=c) (λ j b => b.modifyM i j (f j)) a

def modifyRowIdx (a : Matrix α r c) (i : Fin r) (f : Fin c → α → α) : Matrix α r c :=
  Id.run <| a.modifyRowIdxM i f

-- Modificaion of a column with row indices
def modifyColIdxM {m : Type _ → Type _} [Monad m] (a : Matrix α r c) (j : Fin c) (f : Fin r → α → m α) : m (Matrix α r c) :=
  Fin.foldAllM (n:=r) (λ i b => b.modifyM i j (f i)) a

def modifyColIdx (a : Matrix α r c) (j : Fin c) (f : Fin r → α → α) : Matrix α r c :=
  Id.run <| a.modifyColIdxM j f

end modifyM

/-!
## Arithmetic operations
-/

section Addition

variable {α β γ : Type _} {r c : Nat}

def zipWith {α : Type u} {β : Type v} {γ : Type w} (f : α → β → γ) (x : Matrix α r c) (y : Matrix β r c) : Matrix γ r c where
  entry := Array.zipWith x.entry y.entry f
  hsize := by rw [Array.zipWith_size, x.hsize, y.hsize, Nat.min_eq]

def add [Add α] : Matrix α r c → Matrix α r c → Matrix α r c := zipWith (·+·)

def hAdd [HAdd α β γ] : Matrix α r c → Matrix β r c → Matrix γ r c := zipWith (·+·)

end Addition

section Multiplication

variable {α β γ : Type _} [ToString α] [ToString β] [ToString γ]{r k c : Nat}

def hMul [HMul α β γ] [HAdd γ γ γ] [OfNat γ (nat_lit 0)] (x : Matrix α r k) (y : Matrix β k c) : Matrix γ r c :=
  ofFn (λ i j => Fin.foldAll (n:=k) (λ s a => a + x.get i s * y.get s j) 0)

end Multiplication

/-!
## BLAS-like interfaces
-/

section BLAS

variable {α : Type u} {β : Type v} {γ : Type w} {r c : Nat}

-- Scalar multiplication on a row from left
def scalarLeftRow [HMul α β β] (a : Matrix β r c) (coeff : α) (i : Fin r) : Matrix β r c :=
  a.modifyRow i (coeff * ·)

-- Scalar multiplication on a row from right
def scalarRightRow [HMul α β α] (a : Matrix α r c) (i : Fin r) (coeff : β) : Matrix α r c :=
  a.modifyRow i (· * coeff)

-- Scalar multiplication on a column from left
def scalarLeftCol [HMul α β β] (a : Matrix β r c) (coeff : α) (j : Fin c) : Matrix β r c :=
  a.modifyCol j (coeff * ·)

-- Scalar multiplication on a column from right
def scalarRightCol [HMul α β α] (a : Matrix α r c) (j : Fin c) (coeff : β) : Matrix α r c :=
  a.modifyCol j (· * coeff)

-- Swap two rows
def swapRow (a : Matrix α r c) (i₁ i₂ : Fin r) : Matrix α r c :=
  Fin.foldAll (n:=c)
    (fun j a => {
      entry := a.entry.swap (a.hsize.symm ▸ Fin.lexFold i₁ j) (a.hsize.symm ▸ Fin.lexFold i₂ j)
      hsize := by rw [Array.size_swap, a.hsize]
    })
    a

-- Swap two columns
def swapCol (a : Matrix α r c) (j₁ j₂ : Fin c) : Matrix α r c :=
  Fin.foldAll (n:=r)
    (fun i a => {
      entry := a.entry.swap (a.hsize.symm ▸ Fin.lexFold i j₁) (a.hsize.symm ▸ Fin.lexFold i j₂)
      hsize := by rw [Array.size_swap, a.hsize]
    })
    a

-- Add a scalar multiple of a row to another
-- The multiplication is performed from left: `y ← a*x + y`
def axpyRow [HMul α β γ] [HAdd γ β β] (a : Matrix β r c) (coeff : α) (isrc : Fin r) (itgt : Fin r) : Matrix β r c:=
  a.modifyRowIdx itgt $
    fun j x => coeff * a.get isrc j + x

-- Add a scalar multiple of a row to another
-- The multiplication is performed from right: `y ← x*a + y`
def xapyRow [HMul α β γ] [HAdd γ α α] (a : Matrix α r c) (isrc : Fin r) (coeff : β) (itgt : Fin r) : Matrix α r c :=
  a.modifyRowIdx itgt $
    fun j x => a.get isrc j * coeff + x

-- Add a scalar multiple of a column to another
-- The multiplication is performed from left: `y ← a*x + y`
def axpyCol [HMul α β γ] [HAdd γ β β] (a : Matrix β r c) (coeff : α) (jsrc : Fin c) (jtgt : Fin c) : Matrix β r c :=
  a.modifyColIdx jtgt $
    fun i x => coeff * a.get i jsrc + x

-- Add a scalar multiple of a column to another
-- The multiplication is performed from right: `y ← x*a + y`
def xapyCol [HMul α β γ] [HAdd γ α α] (a : Matrix α r c) (jsrc : Fin c) (coeff : β) (jtgt : Fin c) : Matrix α r c :=
  a.modifyColIdx jtgt $
    fun i x => a.get i jsrc * coeff + x

end BLAS

end Matrix

author: Junology

repo: algdata

save_path: github-repos/lean/Junology-algdata


text:
/-
Copyright (c) 2022 Yaël Dillies. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yaël Dillies
-/
import tactic.split_ifs

/-!
# More basic logic properties

A few more logic lemmas. These are in their own file, rather than `logic.basic`, because it is
convenient to be able to use the `split_ifs` tactic.

## Implementation notes

We spell those lemmas out with `dite` and `ite` rather than the `if then else` notation because this
would result in less delta-reduced statements.
-/

variables {α : Sort*} {p q r : Prop} [decidable p] [decidable q] {a b c : α}

lemma dite_dite_distrib_left {a : p → α} {b : ¬ p → q → α} {c : ¬ p → ¬ q → α} :
  dite p a (λ hp, dite q (b hp) (c hp)) =
    dite q (λ hq, dite p a $ λ hp, b hp hq) (λ hq, dite p a $ λ hp, c hp hq) :=
by split_ifs; refl

lemma dite_dite_distrib_right {a : p → q → α} {b : p → ¬ q → α} {c : ¬ p → α} :
  dite p (λ hp, dite q (a hp) (b hp)) c =
    dite q (λ hq, dite p (λ hp, a hp hq) c) (λ hq, dite p (λ hp, b hp hq) c) :=
by split_ifs; refl

lemma ite_dite_distrib_left {a : α} {b : q → α} {c : ¬ q → α} :
  ite p a (dite q b c) = dite q (λ hq, ite p a $ b hq) (λ hq, ite p a $ c hq) :=
dite_dite_distrib_left

lemma ite_dite_distrib_right {a : q → α} {b : ¬ q → α} {c : α} :
  ite p (dite q a b) c = dite q (λ hq, ite p (a hq) c) (λ hq, ite p (b hq) c) :=
dite_dite_distrib_right

lemma dite_ite_distrib_left {a : p → α} {b : ¬ p → α} {c : ¬ p → α} :
  dite p a (λ hp, ite q (b hp) (c hp)) = ite q (dite p a b) (dite p a c) :=
dite_dite_distrib_left

lemma dite_ite_distrib_right {a : p → α} {b : p → α} {c : ¬ p → α} :
  dite p (λ hp, ite q (a hp) (b hp)) c = ite q (dite p a c) (dite p b c) :=
dite_dite_distrib_right

lemma ite_ite_distrib_left : ite p a (ite q b c) = ite q (ite p a b) (ite p a c) :=
dite_dite_distrib_left

lemma ite_ite_distrib_right : ite p (ite q a b) c = ite q (ite p a c) (ite p b c) :=
dite_dite_distrib_right

author: nick-kuhn

repo: leantools

save_path: github-repos/lean/nick-kuhn-leantools