michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(library/algebra/category/morphism): make sure bug #231 has been fixed

Browse source
This commit is contained in:
Leonardo de Moura 2014-10-13 20:56:40 -07:00
parent b7c1b348d1
commit 4a9e725ca7
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
library/algebra/category/morphism.lean
View file

@ -9,12 +9,12 @@ open eq eq.ops category
namespace morphism namespace morphism
section section
variables {ob : Type} [C : category ob] include C variables {ob : Type} [C : category ob] include C
variables {a b c d : ob} {h : @hom ob C c d} {g : @hom ob C b c} {f : @hom ob C a b} {i : @hom ob C b a} variables {a b c d : ob} {h : hom c d} {g : hom b c} {f : hom a b} {i : hom b a}
inductive is_section [class] (f : @hom ob C a b) : Type inductive is_section [class] (f : hom a b) : Type
:= mk : ∀{g}, g ∘ f = id → is_section f := mk : ∀{g}, g ∘ f = id → is_section f
inductive is_retraction [class] (f : @hom ob C a b) : Type inductive is_retraction [class] (f : hom a b) : Type
:= mk : ∀{g}, f ∘ g = id → is_retraction f := mk : ∀{g}, f ∘ g = id → is_retraction f
inductive is_iso [class] (f : @hom ob C a b) : Type inductive is_iso [class] (f : hom a b) : Type
:= mk : ∀{g}, g ∘ f = id → f ∘ g = id → is_iso f := mk : ∀{g}, g ∘ f = id → f ∘ g = id → is_iso f
--remove implicit arguments in above lines --remove implicit arguments in above lines
definition retraction_of (f : hom a b) [H : is_section f] : hom b a := definition retraction_of (f : hom a b) [H : is_section f] : hom b a :=