%--------------------------------------------------------------------------
% File     : S5LAxioms+0 : TPTP v0.0.0. Released v0.0.0.
% Domain   : Homological Algebra
% Axioms   : Homological algebra axioms
% Version  : [TPTP] axioms.
% English  :

% Refs     :
% Source   : [TPTP]
% Names    :

% Status   : 
% Syntax   : Number of formulae    :   13 (   0 unit)
%            Number of atoms       :   64 (  16 equality)
%            Maximal formula depth :    9 (   6 average)
%            Number of connectives :   51 (   0 ~  ;   0  |;  28  &)
%                                         (   2 <=>;  21 =>;   0 <=)
%                                         (   0 <~>;   0 ~|;   0 ~&)
%            Number of predicates  :    7 (   0 propositional; 1-4 arity)
%            Number of functors    :    3 (   0 constant; 1-3 arity)
%            Number of variables   :   67 (   0 singleton;  63 !;   4 ?)
%            Maximal term depth    :    3 (   1 average)

% Comments : 
%--------------------------------------------------------------------------
input_formula(morphism,axiom,(
    ! [Morphism,Dom,Cod] : 
      ( morphism(Morphism,Dom,Cod)
     => ( ! [El] : 
            ( element(El,Dom)
           => element(apply(Morphism,El),Cod) )
        & equal(apply(Morphism,zero(Dom)),zero(Cod)) ) )   )).

input_formula(injection_properties,axiom,(
    ! [Morphism,Dom,Cod] : 
      ( ( injection(Morphism)
        & morphism(Morphism,Dom,Cod) )
     => ! [El] : 
          ( ( element(El,Dom)
            & equal(apply(Morphism,El),zero(Cod)) )
         => equal(El,zero(Dom)) ) )   )).

input_formula(properties_for_injection,axiom,(
    ! [Morphism,Dom,Cod] : 
      ( ( morphism(Morphism,Dom,Cod)
        & ! [El] : 
            ( ( element(El,Dom)
              & equal(apply(Morphism,El),zero(Cod)) )
           => equal(El,zero(Dom)) ) )
     => injection(Morphism) )   )).

input_formula(surjection_properties,axiom,(
    ! [Morphism,Dom,Cod] : 
      ( ( surjection(Morphism)
        & morphism(Morphism,Dom,Cod) )
     => ! [ElCod] : 
          ( element(ElCod,Cod)
         => ? [ElDom] : 
              ( element(ElDom,Dom)
              & equal(apply(Morphism,ElDom),ElCod) ) ) )   )).

input_formula(properties_for_surjection,axiom,(
    ! [Morphism,Dom,Cod] : 
      ( ( morphism(Morphism,Dom,Cod)
        & ! [ElCod] : 
            ( element(ElCod,Cod)
           => ? [ElDom] : 
                ( element(ElDom,Dom)
                & equal(apply(Morphism,ElDom),ElCod) ) ) )
     => surjection(Morphism) )   )).

input_formula(exact_properties,axiom,(
    ! [Morphism1,Morphism2,Dom,CodDom,Cod] : 
      ( ( exact(Morphism1,Morphism2)
        & morphism(Morphism1,Dom,CodDom)
        & morphism(Morphism2,CodDom,Cod) )
     => ! [ElCodDom] : 
          ( ( element(ElCodDom,CodDom)
            & equal(apply(Morphism2,ElCodDom),zero(Cod)) )
        <=> ? [ElDom] : 
              ( element(ElDom,Dom)
              & equal(apply(Morphism1,ElDom),ElCodDom) ) ) )   )).

input_formula(properties_for_exact,axiom,(
    ! [Morphism1,Morphism2,Dom,CodDom,Cod] : 
      ( ( morphism(Morphism1,Dom,CodDom)
        & morphism(Morphism2,CodDom,Cod)
        & ! [ElCodDom] : 
            ( ( element(ElCodDom,CodDom)
              & equal(apply(Morphism2,ElCodDom),zero(Cod)) )
          <=> ? [ElDom] : 
                ( element(ElDom,Dom)
                & equal(apply(Morphism1,ElDom),ElCodDom) ) ) )
     => exact(Morphism1,Morphism2) )   )).

input_formula(commute_properties,axiom,(
    ! [M1,M2,M3,M4,Dom,DomCod1,DomCod2,Cod] : 
      ( ( commute(M1,M2,M3,M4)
        & morphism(M1,Dom,DomCod1)
        & morphism(M2,DomCod1,Cod)
        & morphism(M3,Dom,DomCod2)
        & morphism(M4,DomCod2,Cod) )
     => ! [ElDom] : 
          ( element(ElDom,Dom)
         => equal(apply(M2,apply(M1,ElDom)),apply(M4,apply(M3,ElDom))) ) )   )).

input_formula(properties_for_commute,axiom,(
    ! [M1,M2,M3,M4,Dom,DomCod1,DomCod2,Cod] : 
      ( ( morphism(M1,Dom,DomCod1)
        & morphism(M2,DomCod1,Cod)
        & morphism(M3,Dom,DomCod2)
        & morphism(M4,DomCod2,Cod)
        & ! [ElDom] : 
            ( element(ElDom,Dom)
           => equal(apply(M2,apply(M1,ElDom)),apply(M4,apply(M3,ElDom))) ) )
     => commute(M1,M2,M3,M4) )   )).

input_formula(subtract_in_domain,axiom,(
    ! [Dom,El1,El2] : 
      ( ( element(El1,Dom)
        & element(El2,Dom) )
     => element(subtract(Dom,El1,El2),Dom) )   )).

input_formula(subtract_to_0,axiom,(
    ! [Dom,El] : 
      ( element(El,Dom)
     => equal(subtract(Dom,El,El),zero(Dom)) )   )).

input_formula(subtract_cancellation,axiom,(
    ! [Dom,El1,El2] : 
      ( ( element(El1,Dom)
        & element(El2,Dom) )
     => equal(subtract(Dom,El1,subtract(Dom,El1,El2)),El2) )   )).

input_formula(subtract_distribution,axiom,(
    ! [Morphism,Dom,Cod] : 
      ( morphism(Morphism,Dom,Cod)
     => ! [El1,El2] : 
          ( ( element(El1,Dom)
            & element(El2,Dom) )
         => equal(apply(Morphism,subtract(Dom,El1,El2)),subtract(Cod,apply(Morphism,El1),apply(Morphism,El2))) ) )   )).
%--------------------------------------------------------------------------