%--------------------------------------------------------------------------
% File     : HAL001+0 : TPTP v7.2.0. Released v2.6.0.
% Domain   : Homological Algebra
% Axioms   : Standard homological algebra axioms
% Version  : [TPTP] axioms.
% English  :

% Refs     : [Wei94] Weibel (1994), An Introduction to Homological Algebra
% Source   : [TPTP]
% Names    :

% Status   : Satisfiable
% Syntax   : Number of formulae    :   13 (   0 unit)
%            Number of atoms       :   66 (  16 equality)
%            Maximal formula depth :   16 (  10 average)
%            Number of connectives :   53 (   0 ~  ;   0  |;  30  &)
%                                         (   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   :   69 (   0 singleton;  65 !;   4 ?)
%            Maximal term depth    :    3 (   1 average)
% SPC      : 

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

fof(injection_properties,axiom,
    ( ! [Morphism,Dom,Cod] :
        ( ( injection(Morphism)
          & morphism(Morphism,Dom,Cod) )
       => ! [El1,El2] :
            ( ( element(El1,Dom)
              & element(El2,Dom)
              & apply(Morphism,El1) = apply(Morphism,El2) )
           => El1 = El2 ) ) )).

fof(properties_for_injection,axiom,
    ( ! [Morphism,Dom,Cod] :
        ( ( morphism(Morphism,Dom,Cod)
          & ! [El1,El2] :
              ( ( element(El1,Dom)
                & element(El2,Dom)
                & apply(Morphism,El1) = apply(Morphism,El2) )
             => El1 = El2 ) )
       => injection(Morphism) ) )).

%----Sasha's weird injection axioms
% 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) )  )).

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

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

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

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

fof(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)
           => apply(M2,apply(M1,ElDom)) = apply(M4,apply(M3,ElDom)) ) ) )).

fof(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)
             => apply(M2,apply(M1,ElDom)) = apply(M4,apply(M3,ElDom)) ) )
       => commute(M1,M2,M3,M4) ) )).

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

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

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

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

%--------------------------------------------------------------------------