C : Type u
inst✝³ : Category C
inst✝² : ConcreteCategory C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C) := (forget C).mapCone D
⊢ Function.Injective fun x j => (forget C).map (D.π.app j) x
C : Type u
inst✝³ : Category C
inst✝² : ConcreteCategory C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
⊢ Function.Injective fun x j => (forget C).map (D.π.app j) x
let E := (forget C).mapCone D
C : Type u
inst✝³ : Category C
inst✝² : ConcreteCategory C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C) := (forget C).mapCone D
hE : IsLimit E := isLimitOfPreserves (forget C) hD
⊢ Function.Injective fun x j => (forget C).map (D.π.app j) x
C : Type u
inst✝³ : Category C
inst✝² : ConcreteCategory C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C) := (forget C).mapCone D
⊢ Function.Injective fun x j => (forget C).map (D.π.app j) x
let hE : IsLimit E := isLimitOfPreserves _ hD
C : Type u
inst✝³ : Category C
inst✝² : ConcreteCategory C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C) := (forget C).mapCone D
hE : IsLimit E := isLimitOfPreserves (forget C) hD
G : Cone (F ⋙ forget C) := Types.limitCone (F ⋙ forget C)
⊢ Function.Injective fun x j => (forget C).map (D.π.app j) x
C : Type u
inst✝³ : Category C
inst✝² : ConcreteCategory C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C) := (forget C).mapCone D
hE : IsLimit E := isLimitOfPreserves (forget C) hD
⊢ Function.Injective fun x j => (forget C).map (D.π.app j) x
let G := Types.limitCone.{w, v} (F ⋙ forget C)
C : Type u
inst✝³ : Category C
inst✝² : ConcreteCategory C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C) := (forget C).mapCone D
hE : IsLimit E := isLimitOfPreserves (forget C) hD
G : Cone (F ⋙ forget C) := Types.limitCone (F ⋙ forget C)
hG : IsLimit (Types.limitCone (F ⋙ forget C)) := Types.limitConeIsLimit (F ⋙ forget C)
⊢ Function.Injective fun x j => (forget C).map (D.π.app j) x
C : Type u
inst✝³ : Category C
inst✝² : ConcreteCategory C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C) := (forget C).mapCone D
hE : IsLimit E := isLimitOfPreserves (forget C) hD
G : Cone (F ⋙ forget C) := Types.limitCone (F ⋙ forget C)
⊢ Function.Injective fun x j => (forget C).map (D.π.app j) x
let hG := Types.limitConeIsLimit.{w, v} (F ⋙ forget C)
C : Type u
inst✝³ : Category C
inst✝² : ConcreteCategory C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C) := (forget C).mapCone D
hE : IsLimit E := isLimitOfPreserves (forget C) hD
G : Cone (F ⋙ forget C) := Types.limitCone (F ⋙ forget C)
hG : IsLimit (Types.limitCone (F ⋙ forget C)) := Types.limitConeIsLimit (F ⋙ forget C)
T : E.pt ≅ G.pt := IsLimit.conePointUniqueUpToIso hE hG
⊢ Function.Injective fun x j => (forget C).map (D.π.app j) x
C : Type u
inst✝³ : Category C
inst✝² : ConcreteCategory C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C) := (forget C).mapCone D
hE : IsLimit E := isLimitOfPreserves (forget C) hD
G : Cone (F ⋙ forget C) := Types.limitCone (F ⋙ forget C)
hG : IsLimit (Types.limitCone (F ⋙ forget C)) := Types.limitConeIsLimit (F ⋙ forget C)
⊢ Function.Injective fun x j => (forget C).map (D.π.app j) x
let T : E.pt ≅ G.pt := hE.conePointUniqueUpToIso hG
C : Type u
inst✝³ : Category C
inst✝² : ConcreteCategory C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C) := (forget C).mapCone D
hE : IsLimit E := isLimitOfPreserves (forget C) hD
G : Cone (F ⋙ forget C) := Types.limitCone (F ⋙ forget C)
hG : IsLimit (Types.limitCone (F ⋙ forget C)) := Types.limitConeIsLimit (F ⋙ forget C)
T : E.pt ≅ G.pt := IsLimit.conePointUniqueUpToIso hE hG
⊢ Function.Injective (T.hom ≫ fun x j => G.π.app j x)
C : Type u
inst✝³ : Category C
inst✝² : ConcreteCategory C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C) := (forget C).mapCone D
hE : IsLimit E := isLimitOfPreserves (forget C) hD
G : Cone (F ⋙ forget C) := Types.limitCone (F ⋙ forget C)
hG : IsLimit (Types.limitCone (F ⋙ forget C)) := Types.limitConeIsLimit (F ⋙ forget C)
T : E.pt ≅ G.pt := IsLimit.conePointUniqueUpToIso hE hG
⊢ Function.Injective fun x j => (forget C).map (D.π.app j) x
change Function.Injective (T.hom ≫ fun x j => G.π.app j x)
C : Type u
inst✝³ : Category C
inst✝² : ConcreteCategory C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C) := (forget C).mapCone D
hE : IsLimit E := isLimitOfPreserves (forget C) hD
G : Cone (F ⋙ forget C) := Types.limitCone (F ⋙ forget C)
hG : IsLimit (Types.limitCone (F ⋙ forget C)) := Types.limitConeIsLimit (F ⋙ forget C)
T : E.pt ≅ G.pt := IsLimit.conePointUniqueUpToIso hE hG
h : Function.Injective T.hom
⊢ Function.Injective (T.hom ≫ fun x j => G.π.app j x)
C : Type u
inst✝³ : Category C
inst✝² : ConcreteCategory C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C) := (forget C).mapCone D
hE : IsLimit E := isLimitOfPreserves (forget C) hD
G : Cone (F ⋙ forget C) := Types.limitCone (F ⋙ forget C)
hG : IsLimit (Types.limitCone (F ⋙ forget C)) := Types.limitConeIsLimit (F ⋙ forget C)
T : E.pt ≅ G.pt := IsLimit.conePointUniqueUpToIso hE hG
⊢ Function.Injective (T.hom ≫ fun x j => G.π.app j x)
have h : Function.Injective T.hom := by
  intro a b h
  suffices T.inv (T.hom a) = T.inv (T.hom b) by simpa
  rw [h]
C : Type u
inst✝³ : Category C
inst✝² : ConcreteCategory C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C) := (forget C).mapCone D
hE : IsLimit E := isLimitOfPreserves (forget C) hD
G : Cone (F ⋙ forget C) := Types.limitCone (F ⋙ forget C)
hG : IsLimit (Types.limitCone (F ⋙ forget C)) := Types.limitConeIsLimit (F ⋙ forget C)
T : E.pt ≅ G.pt := IsLimit.conePointUniqueUpToIso hE hG
h : Function.Injective T.hom
⊢ Function.Injective fun x j => G.π.app j x
C : Type u
inst✝³ : Category C
inst✝² : ConcreteCategory C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C) := (forget C).mapCone D
hE : IsLimit E := isLimitOfPreserves (forget C) hD
G : Cone (F ⋙ forget C) := Types.limitCone (F ⋙ forget C)
hG : IsLimit (Types.limitCone (F ⋙ forget C)) := Types.limitConeIsLimit (F ⋙ forget C)
T : E.pt ≅ G.pt := IsLimit.conePointUniqueUpToIso hE hG
h : Function.Injective T.hom
⊢ Function.Injective (T.hom ≫ fun x j => G.π.app j x)
suffices Function.Injective fun (x : G.pt) j => G.π.app j x by exact this.comp h
no goals
C : Type u
inst✝³ : Category C
inst✝² : ConcreteCategory C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C) := (forget C).mapCone D
hE : IsLimit E := isLimitOfPreserves (forget C) hD
G : Cone (F ⋙ forget C) := Types.limitCone (F ⋙ forget C)
hG : IsLimit (Types.limitCone (F ⋙ forget C)) := Types.limitConeIsLimit (F ⋙ forget C)
T : E.pt ≅ G.pt := IsLimit.conePointUniqueUpToIso hE hG
h : Function.Injective T.hom
⊢ Function.Injective fun x j => G.π.app j x
apply Subtype.ext
C : Type u
inst✝³ : Category C
inst✝² : ConcreteCategory C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C) := (forget C).mapCone D
hE : IsLimit E := isLimitOfPreserves (forget C) hD
G : Cone (F ⋙ forget C) := Types.limitCone (F ⋙ forget C)
hG : IsLimit (Types.limitCone (F ⋙ forget C)) := Types.limitConeIsLimit (F ⋙ forget C)
T : E.pt ≅ G.pt := IsLimit.conePointUniqueUpToIso hE hG
a b : E.pt
h : T.hom a = T.hom b
⊢ a = b
C : Type u
inst✝³ : Category C
inst✝² : ConcreteCategory C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C) := (forget C).mapCone D
hE : IsLimit E := isLimitOfPreserves (forget C) hD
G : Cone (F ⋙ forget C) := Types.limitCone (F ⋙ forget C)
hG : IsLimit (Types.limitCone (F ⋙ forget C)) := Types.limitConeIsLimit (F ⋙ forget C)
T : E.pt ≅ G.pt := IsLimit.conePointUniqueUpToIso hE hG
⊢ Function.Injective T.hom
intro a b h
C : Type u
inst✝³ : Category C
inst✝² : ConcreteCategory C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C) := (forget C).mapCone D
hE : IsLimit E := isLimitOfPreserves (forget C) hD
G : Cone (F ⋙ forget C) := Types.limitCone (F ⋙ forget C)
hG : IsLimit (Types.limitCone (F ⋙ forget C)) := Types.limitConeIsLimit (F ⋙ forget C)
T : E.pt ≅ G.pt := IsLimit.conePointUniqueUpToIso hE hG
a b : E.pt
h : T.hom a = T.hom b
⊢ T.inv (T.hom a) = T.inv (T.hom b)
C : Type u
inst✝³ : Category C
inst✝² : ConcreteCategory C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C) := (forget C).mapCone D
hE : IsLimit E := isLimitOfPreserves (forget C) hD
G : Cone (F ⋙ forget C) := Types.limitCone (F ⋙ forget C)
hG : IsLimit (Types.limitCone (F ⋙ forget C)) := Types.limitConeIsLimit (F ⋙ forget C)
T : E.pt ≅ G.pt := IsLimit.conePointUniqueUpToIso hE hG
a b : E.pt
h : T.hom a = T.hom b
⊢ a = b
suffices T.inv (T.hom a) = T.inv (T.hom b) by simpa
no goals
C : Type u
inst✝³ : Category C
inst✝² : ConcreteCategory C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C) := (forget C).mapCone D
hE : IsLimit E := isLimitOfPreserves (forget C) hD
G : Cone (F ⋙ forget C) := Types.limitCone (F ⋙ forget C)
hG : IsLimit (Types.limitCone (F ⋙ forget C)) := Types.limitConeIsLimit (F ⋙ forget C)
T : E.pt ≅ G.pt := IsLimit.conePointUniqueUpToIso hE hG
a b : E.pt
h : T.hom a = T.hom b
⊢ T.inv (T.hom a) = T.inv (T.hom b)
rw [h]
no goals
C : Type u
inst✝³ : Category C
inst✝² : ConcreteCategory C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C) := (forget C).mapCone D
hE : IsLimit E := isLimitOfPreserves (forget C) hD
G : Cone (F ⋙ forget C) := Types.limitCone (F ⋙ forget C)
hG : IsLimit (Types.limitCone (F ⋙ forget C)) := Types.limitConeIsLimit (F ⋙ forget C)
T : E.pt ≅ G.pt := IsLimit.conePointUniqueUpToIso hE hG
a b : E.pt
h : T.hom a = T.hom b
this : T.inv (T.hom a) = T.inv (T.hom b)
⊢ a = b
simpa
no goals
C : Type u
inst✝³ : Category C
inst✝² : ConcreteCategory C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C) := (forget C).mapCone D
hE : IsLimit E := isLimitOfPreserves (forget C) hD
G : Cone (F ⋙ forget C) := Types.limitCone (F ⋙ forget C)
hG : IsLimit (Types.limitCone (F ⋙ forget C)) := Types.limitConeIsLimit (F ⋙ forget C)
T : E.pt ≅ G.pt := IsLimit.conePointUniqueUpToIso hE hG
h : Function.Injective T.hom
this : Function.Injective fun x j => G.π.app j x
⊢ Function.Injective (T.hom ≫ fun x j => G.π.app j x)
exact this.comp h